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