# HG changeset patch
# User wenzelm
# Date 963522855 -7200
# Node ID 7a72952ca06801c915213725a14274c69757fb23
# Parent  e58778cc4d22ccd7cc84c4276c81a19e1d3b3231
adapted PureThy.add_defs;

diff -r e58778cc4d22 -r 7a72952ca068 src/HOLCF/IOA/meta_theory/ioa_package.ML
--- 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)