--- 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)
--- 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 =
--- 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;
--- 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)