From 5d70cb49af478e1db70be48c414c3114878494ae Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Fri, 24 Jun 2016 17:13:26 +1000 Subject: [PATCH] Fix bug identified in b1f6ab1 --- src/tfl/src/Defn.sml | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/src/tfl/src/Defn.sml b/src/tfl/src/Defn.sml index 61c01686aa..97637f9aba 100644 --- a/src/tfl/src/Defn.sml +++ b/src/tfl/src/Defn.sml @@ -1740,17 +1740,14 @@ end fun parse_absyn absyn0 = let val (absyn,fn_names) = elim_wildcards absyn0 - val oinfo = term_grammar.overload_info (term_grammar()) + val oldg = term_grammar() + val oinfo = term_grammar.overload_info oldg val nonconstructor_parameter_names = List.filter (not o is_constructor_name oinfo) (get_param_names absyn) - val to_restore = - map (fn s => (s,Parse.hide s)) (nonconstructor_parameter_names @ fn_names) - fun restore() = List.app (uncurry Parse.update_overload_maps) to_restore + val _ = + app (ignore o Parse.hide) (nonconstructor_parameter_names @ fn_names) + fun restore() = temp_set_grammars(type_grammar(), oldg) val tm = defn_absyn_to_term absyn handle e => (restore(); raise e) -(* Old parsing of abstract syntax: - val tm = Parse.absyn_to_term (Parse.term_grammar()) absyn - handle e => (restore(); raise e) -*) in restore(); (tm, fn_names)