--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Thu Jul 13 23:13:52 2000 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Thu Jul 13 23:14:15 2000 +0200
@@ -360,7 +360,7 @@
(automaton_name ^ "_trans",
"(" ^ action_type ^ "," ^ state_type_string ^ ")transition set" ,NoSyn),
(automaton_name, "(" ^ action_type ^ "," ^ state_type_string ^ ")ioa" ,NoSyn)]
-|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
+|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
[(automaton_name ^ "_initial_def",
automaton_name ^ "_initial == {" ^ state_vars_tupel ^ "." ^ ini ^ "}"),
(automaton_name ^ "_asig_def",
@@ -401,7 +401,7 @@
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
-|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
+|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == " ^ comp_list)]
end)
@@ -416,7 +416,7 @@
thy
|> ContConsts.add_consts_i
[(automaton_name, auttyp,NoSyn)]
-|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
+|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == restrict " ^ aut_source ^ " " ^ rest_set)]
end)
@@ -430,7 +430,7 @@
thy
|> ContConsts.add_consts_i
[(automaton_name, auttyp,NoSyn)]
-|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
+|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == hide " ^ aut_source ^ " " ^ hid_set)]
end)
@@ -462,7 +462,7 @@
Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
-|> (#1 oo (PureThy.add_defs o map Thm.no_attributes))
+|> (#1 oo (PureThy.add_defs false o map Thm.no_attributes))
[(automaton_name ^ "_def",
automaton_name ^ " == rename " ^ aut_source ^ " (" ^ fun_name ^ ")")]
end)