--- a/src/HOLCF/IOA/meta_theory/automaton.ML Mon Jul 12 21:12:18 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML Mon Jul 12 21:38:37 2010 +0200
@@ -131,7 +131,7 @@
(* making a constructor set from a constructor term (of signature) *)
fun constr_set_string thy atyp ctstr =
let
-val trm = OldGoals.simple_read_term thy atyp ctstr;
+val trm = Misc_Legacy.simple_read_term thy atyp ctstr;
val l = free_vars_of trm
in
if (check_for_constr thy atyp trm) then
@@ -148,7 +148,7 @@
fun hd_of (Const(a,_)) = a |
hd_of (t $ _) = hd_of t |
hd_of _ = raise malformed;
-val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
+val trm = Misc_Legacy.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
in
hd_of trm handle malformed =>
error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
@@ -177,8 +177,8 @@
(where bool indicates whether there is a precondition *)
fun extend thy atyp statetupel (actstr,r,[]) =
let
-val trm = OldGoals.simple_read_term thy atyp actstr;
-val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
+val trm = Misc_Legacy.simple_read_term thy atyp actstr;
+val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r;
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm)
@@ -191,8 +191,8 @@
fun pseudo_poststring [] = "" |
pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r);
-val trm = OldGoals.simple_read_term thy atyp actstr;
-val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
+val trm = Misc_Legacy.simple_read_term thy atyp actstr;
+val rtrm = Misc_Legacy.simple_read_term thy (Type("bool",[])) r;
val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
in
if (check_for_constr thy atyp trm) then
@@ -366,7 +366,7 @@
automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
"_initial, " ^ automaton_name ^ "_trans,{},{})")
])
-val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
+val chk_prime_list = (check_free_primed (Misc_Legacy.simple_read_term thy2 (Type("bool",[]))
( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
in
(