OldGoals.simple_read_term;
authorwenzelm
Wed Jun 18 18:54:59 2008 +0200 (2008-06-18)
changeset 27251121991a4884d
parent 27250 7eef2b183032
child 27252 042aebff17e1
OldGoals.simple_read_term;
src/HOL/Modelcheck/mucke_oracle.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/Pure/Proof/extraction.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed Jun 18 18:54:57 2008 +0200
     1.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed Jun 18 18:54:59 2008 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4    fun deliver_erg sg tl _ [] = [] |
     1.5    deliver_erg sg tl typ ((c,tyl)::r) = let
     1.6                          val ft = fun_type_of (rev tyl) typ;
     1.7 -                        val trm = Sign.simple_read_term sg ft c;
     1.8 +                        val trm = OldGoals.simple_read_term sg ft c;
     1.9                          in
    1.10                          (con_term_list_of trm (arglist_of sg tl tyl))
    1.11  			@(deliver_erg sg tl typ r)
    1.12 @@ -658,7 +658,7 @@
    1.13   val arglist = arglist_of sg tl (snd c);
    1.14   val tty = type_of_term t;
    1.15   val con_typ = fun_type_of (rev (snd c)) tty;
    1.16 - val con = Sign.simple_read_term sg con_typ (fst c);
    1.17 + val con = OldGoals.simple_read_term sg con_typ (fst c);
    1.18  in
    1.19   replace_termlist_with_args sg tl a con arglist t (l1,l2)
    1.20  end |
    1.21 @@ -746,7 +746,7 @@
    1.22  let
    1.23   val arglist = arglist_of sg tl (snd c);
    1.24   val con_typ = fun_type_of (rev (snd c)) ty;
    1.25 - val con = Sign.simple_read_term sg con_typ (fst c);
    1.26 + val con = OldGoals.simple_read_term sg con_typ (fst c);
    1.27   fun casc_if2 sg tl x con [] ty trm [] = trm | (* should never occur *)
    1.28   casc_if2 sg tl x con [arg] ty trm [] = x_subst sg tl x (con_term_of con arg) trm |
    1.29   casc_if2 sg tl x con (a::r) ty trm cl =
     2.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Jun 18 18:54:57 2008 +0200
     2.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Wed Jun 18 18:54:59 2008 +0200
     2.3 @@ -132,7 +132,7 @@
     2.4  (* making a constructor set from a constructor term (of signature) *)
     2.5  fun constr_set_string thy atyp ctstr =
     2.6  let
     2.7 -val trm = Sign.simple_read_term thy atyp ctstr;
     2.8 +val trm = OldGoals.simple_read_term thy atyp ctstr;
     2.9  val l = free_vars_of trm
    2.10  in
    2.11  if (check_for_constr thy atyp trm) then
    2.12 @@ -149,7 +149,7 @@
    2.13  fun hd_of (Const(a,_)) = a |
    2.14  hd_of (t $ _) = hd_of t |
    2.15  hd_of _ = raise malformed;
    2.16 -val trm = Sign.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
    2.17 +val trm = OldGoals.simple_read_term thy (Syntax.read_typ_global thy atypstr) s;
    2.18  in
    2.19  hd_of trm handle malformed =>
    2.20  error("malformed constructor of datatype " ^ atypstr ^ ": " ^ s)
    2.21 @@ -177,8 +177,8 @@
    2.22  (where bool indicates whether there is a precondition *)
    2.23  fun extend thy atyp statetupel (actstr,r,[]) =
    2.24  let
    2.25 -val trm = Sign.simple_read_term thy atyp actstr;
    2.26 -val rtrm = Sign.simple_read_term thy (Type("bool",[])) r;
    2.27 +val trm = OldGoals.simple_read_term thy atyp actstr;
    2.28 +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
    2.29  val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
    2.30  in
    2.31  if (check_for_constr thy atyp trm)
    2.32 @@ -191,8 +191,8 @@
    2.33  fun pseudo_poststring [] = "" |
    2.34  pseudo_poststring ((a,b)::[]) = "(" ^ a ^ " = (" ^ b ^ "))" |
    2.35  pseudo_poststring ((a,b)::r) = "(" ^ a ^ " = (" ^ b ^ ")) & " ^ (pseudo_poststring r); 
    2.36 -val trm = Sign.simple_read_term thy atyp actstr;
    2.37 -val rtrm = Sign.simple_read_term thy (Type("bool",[])) r;
    2.38 +val trm = OldGoals.simple_read_term thy atyp actstr;
    2.39 +val rtrm = OldGoals.simple_read_term thy (Type("bool",[])) r;
    2.40  val flag = if (rtrm=Const("True",Type("bool",[]))) then false else true
    2.41  in
    2.42  if (check_for_constr thy atyp trm) then
    2.43 @@ -364,7 +364,7 @@
    2.44  automaton_name ^ " == (" ^ automaton_name ^ "_asig, " ^ automaton_name ^
    2.45  "_initial, " ^ automaton_name ^ "_trans,{},{})")
    2.46  ])
    2.47 -val chk_prime_list = (check_free_primed (Sign.simple_read_term thy2 (Type("bool",[]))
    2.48 +val chk_prime_list = (check_free_primed (OldGoals.simple_read_term thy2 (Type("bool",[]))
    2.49  ( "case act_of_" ^ automaton_name ^ " of " ^ snd(alt_string))))
    2.50  in
    2.51  (
     3.1 --- a/src/Pure/Proof/extraction.ML	Wed Jun 18 18:54:57 2008 +0200
     3.2 +++ b/src/Pure/Proof/extraction.ML	Wed Jun 18 18:54:59 2008 +0200
     3.3 @@ -319,7 +319,7 @@
     3.4        val T = etype_of thy' vs [] prop;
     3.5        val (T', thw) = Type.freeze_thaw_type
     3.6          (if T = nullT then nullT else map fastype_of vars' ---> T);
     3.7 -      val t = map_types thw (Sign.simple_read_term thy' T' s1);
     3.8 +      val t = map_types thw (OldGoals.simple_read_term thy' T' s1);
     3.9        val r' = freeze_thaw (condrew thy' eqns
    3.10          (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))
    3.11            (Const ("realizes", T --> propT --> propT) $
     4.1 --- a/src/Pure/codegen.ML	Wed Jun 18 18:54:57 2008 +0200
     4.2 +++ b/src/Pure/codegen.ML	Wed Jun 18 18:54:59 2008 +0200
     4.3 @@ -890,7 +890,7 @@
     4.4    end;
     4.5  
     4.6  val generate_code_i = gen_generate_code Sign.cert_term;
     4.7 -val generate_code = gen_generate_code Sign.read_term;
     4.8 +val generate_code = gen_generate_code OldGoals.read_term;
     4.9  
    4.10  
    4.11  (**** Reflection ****)
    4.12 @@ -1136,7 +1136,7 @@
    4.13          P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >>
    4.14       (fn xs => Toplevel.theory (fn thy => fold (assoc_const o
    4.15         (fn ((const, mfx), aux) =>
    4.16 -         (const, (parse_mixfix (Sign.read_term thy) mfx, aux)))) xs thy)));
    4.17 +         (const, (parse_mixfix (OldGoals.read_term thy) mfx, aux)))) xs thy)));
    4.18  
    4.19  fun parse_code lib =
    4.20    Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) --