# HG changeset patch # User wenzelm # Date 1236465058 -3600 # Node ID 90efbb8a8cb2a60343500edc3217a7c48fb597fc # Parent 76fd85bbf139ae2e437cfdf726ce9e5dde96bd8f minimal adaptions for abstract binding type; diff -r 76fd85bbf139 -r 90efbb8a8cb2 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Sat Mar 07 22:17:25 2009 +0100 +++ b/src/HOL/Import/proof_kernel.ML Sat Mar 07 23:30:58 2009 +0100 @@ -1926,7 +1926,8 @@ val csyn = mk_syn thy constname val thy1 = case HOL4DefThy.get thy of Replaying _ => thy - | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; Sign.add_consts_i [(constname,ctype,csyn)] thy) + | _ => (ImportRecorder.add_consts [(constname, ctype, csyn)]; + Sign.add_consts_i [(Binding.name constname,ctype,csyn)] thy) val eq = mk_defeq constname rhs' thy1 val (thms, thy2) = PureThy.add_defs false [((Binding.name thmname,eq),[])] thy1 val _ = ImportRecorder.add_defs thmname eq @@ -2017,7 +2018,7 @@ val thy' = add_dump str thy val _ = ImportRecorder.add_consts consts in - Sign.add_consts_i consts thy' + Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) consts) thy' end val thy1 = List.foldr (fn(name,thy)=> @@ -2093,7 +2094,9 @@ val tnames = map fst tfrees val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) - val ((_, typedef_info), thy') = TypedefPackage.add_typedef false (SOME thmname) typ c NONE (rtac th2 1) thy + val ((_, typedef_info), thy') = + TypedefPackage.add_typedef false (SOME (Binding.name thmname)) + (Binding.name tycname, tnames, tsyn) c NONE (rtac th2 1) thy val _ = ImportRecorder.add_typedef (SOME thmname) typ c NONE th2 val th3 = (#type_definition typedef_info) RS typedef_hol2hol4 @@ -2179,7 +2182,9 @@ val tnames = sort string_ord (map fst tfrees) val tsyn = mk_syn thy tycname val typ = (tycname,tnames,tsyn) - val ((_, typedef_info), thy') = TypedefPackage.add_typedef false NONE typ c (SOME(rep_name,abs_name)) (rtac th2 1) thy + val ((_, typedef_info), thy') = + TypedefPackage.add_typedef false NONE (Binding.name tycname,tnames,tsyn) c + (SOME(Binding.name rep_name,Binding.name abs_name)) (rtac th2 1) thy val _ = ImportRecorder.add_typedef NONE typ c (SOME(rep_name,abs_name)) th2 val fulltyname = Sign.intern_type thy' tycname val aty = Type (fulltyname, map mk_vartype tnames) diff -r 76fd85bbf139 -r 90efbb8a8cb2 src/HOL/Import/replay.ML --- a/src/HOL/Import/replay.ML Sat Mar 07 22:17:25 2009 +0100 +++ b/src/HOL/Import/replay.ML Sat Mar 07 23:30:58 2009 +0100 @@ -334,7 +334,7 @@ add_hol4_mapping thyname thmname isaname thy | delta (Hol_pending (thyname, thmname, th)) thy = add_hol4_pending thyname thmname ([], th_of thy th) thy - | delta (Consts cs) thy = Sign.add_consts_i cs thy + | delta (Consts cs) thy = Sign.add_consts_i (map (fn (c, T, mx) => (Binding.name c, T, mx)) cs) thy | delta (Hol_const_mapping (thyname, constname, fullcname)) thy = add_hol4_const_mapping thyname constname true fullcname thy | delta (Hol_move (fullname, moved_thmname)) thy = @@ -343,8 +343,9 @@ snd (PureThy.add_defs false [((Binding.name thmname, eq), [])] thy) | delta (Hol_theorem (thyname, thmname, th)) thy = add_hol4_theorem thyname thmname ([], th_of thy th) thy - | delta (Typedef (thmname, typ, c, repabs, th)) thy = - snd (TypedefPackage.add_typedef false thmname typ c repabs (rtac (th_of thy th) 1) thy) + | delta (Typedef (thmname, (t, vs, mx), c, repabs, th)) thy = + snd (TypedefPackage.add_typedef false (Option.map Binding.name thmname) (Binding.name t, vs, mx) c + (Option.map (pairself Binding.name) repabs) (rtac (th_of thy th) 1) thy) | delta (Hol_type_mapping (thyname, tycname, fulltyname)) thy = add_hol4_type_mapping thyname tycname true fulltyname thy | delta (Indexed_theorem (i, th)) thy = diff -r 76fd85bbf139 -r 90efbb8a8cb2 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sat Mar 07 22:17:25 2009 +0100 +++ b/src/HOL/Statespace/state_space.ML Sat Mar 07 23:30:58 2009 +0100 @@ -154,13 +154,13 @@ fun add_locale name expr elems thy = thy - |> Expression.add_locale name name expr elems + |> Expression.add_locale (Binding.name name) (Binding.name name) expr elems |> snd |> LocalTheory.exit; fun add_locale_cmd name expr elems thy = thy - |> Expression.add_locale_cmd name "" expr elems + |> Expression.add_locale_cmd (Binding.name name) Binding.empty expr elems |> snd |> LocalTheory.exit; diff -r 76fd85bbf139 -r 90efbb8a8cb2 src/HOLCF/IOA/meta_theory/ioa_package.ML --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Mar 07 22:17:25 2009 +0100 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Sat Mar 07 23:30:58 2009 +0100 @@ -324,6 +324,8 @@ clist [a] = a | clist (a::r) = a ^ " || " ^ (clist r); +val add_defs = snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes o map (apfst Binding.name)); + (* add_ioa *) @@ -351,7 +353,7 @@ (automaton_name ^ "_trans", "(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn), (automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)] -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes)) +|> add_defs [(automaton_name ^ "_initial_def", automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"), (automaton_name ^ "_asig_def", @@ -392,7 +394,7 @@ Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) ,NoSyn)] -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes)) +|> add_defs [(automaton_name ^ "_def", automaton_name ^ " == " ^ comp_list)] end) @@ -407,7 +409,7 @@ thy |> ContConsts.add_consts_i [(automaton_name, auttyp,NoSyn)] -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes)) +|> add_defs [(automaton_name ^ "_def", automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)] end) @@ -421,7 +423,7 @@ thy |> ContConsts.add_consts_i [(automaton_name, auttyp,NoSyn)] -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes)) +|> add_defs [(automaton_name ^ "_def", automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)] end) @@ -447,7 +449,7 @@ Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]), Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])]) ,NoSyn)] -|> (snd oo (PureThy.add_defs_cmd false o map Thm.no_attributes)) +|> add_defs [(automaton_name ^ "_def", automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")] end)