cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
authorwenzelm
Sat Apr 14 17:36:09 2007 +0200 (2007-04-14)
changeset 226819d42e5365ad1
parent 22680 31a2303f4283
child 22682 92448396c9d9
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
Term.string_of_vname;
src/Pure/Isar/rule_insts.ML
src/Pure/drule.ML
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Sat Apr 14 17:36:07 2007 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat Apr 14 17:36:09 2007 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4  
     1.5  fun is_tvar (x, _) = String.isPrefix "'" x;
     1.6  
     1.7 -fun error_var msg xi = error (msg ^ Syntax.string_of_vname xi);
     1.8 +fun error_var msg xi = error (msg ^ Term.string_of_vname xi);
     1.9  
    1.10  fun the_sort tvars xi = the (AList.lookup (op =) tvars xi)
    1.11    handle Option.Option => error_var "No such type variable in theorem: " xi;
    1.12 @@ -235,15 +235,14 @@
    1.13          val (types, sorts) = types_sorts st;
    1.14      (* Process type insts: Tinsts_env *)
    1.15      fun absent xi = error
    1.16 -          ("No such variable in theorem: " ^ Syntax.string_of_vname xi);
    1.17 +          ("No such variable in theorem: " ^ Term.string_of_vname xi);
    1.18      val (rtypes, rsorts) = types_sorts thm;
    1.19      fun readT (xi, s) =
    1.20          let val S = case rsorts xi of SOME S => S | NONE => absent xi;
    1.21 -            val T = Sign.read_typ (thy, sorts) s;
    1.22 +            val T = Sign.read_def_typ (thy, sorts) s;
    1.23              val U = TVar (xi, S);
    1.24          in if Sign.typ_instance thy (T, U) then (U, T)
    1.25 -           else error
    1.26 -             ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails")
    1.27 +           else error ("Instantiation of " ^ Term.string_of_vname xi ^ " fails")
    1.28          end;
    1.29      val Tinsts_env = map readT Tinsts;
    1.30      (* Preprocess rule: extract vars and their types, apply Tinsts *)
     2.1 --- a/src/Pure/drule.ML	Sat Apr 14 17:36:07 2007 +0200
     2.2 +++ b/src/Pure/drule.ML	Sat Apr 14 17:36:09 2007 +0200
     2.3 @@ -253,10 +253,10 @@
     2.4  (** reading of instantiations **)
     2.5  
     2.6  fun absent ixn =
     2.7 -  error("No such variable in term: " ^ Syntax.string_of_vname ixn);
     2.8 +  error("No such variable in term: " ^ Term.string_of_vname ixn);
     2.9  
    2.10  fun inst_failure ixn =
    2.11 -  error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
    2.12 +  error("Instantiation of " ^ Term.string_of_vname ixn ^ " fails");
    2.13  
    2.14  fun read_insts thy (rtypes,rsorts) (types,sorts) used insts =
    2.15  let
    2.16 @@ -266,7 +266,7 @@
    2.17      fun sort_of ixn = case rsorts ixn of SOME S => S | NONE => absent ixn;
    2.18      fun readT (ixn, st) =
    2.19          let val S = sort_of ixn;
    2.20 -            val T = Sign.read_typ (thy,sorts) st;
    2.21 +            val T = Sign.read_def_typ (thy,sorts) st;
    2.22          in if Sign.typ_instance thy (T, TVar(ixn,S)) then (ixn,T)
    2.23             else inst_failure ixn
    2.24          end
    2.25 @@ -277,7 +277,7 @@
    2.26      val ixnsTs = map mkty vs;
    2.27      val ixns = map fst ixnsTs
    2.28      and sTs  = map snd ixnsTs
    2.29 -    val (cts,tye2) = read_def_cterms(thy,types,sorts) used false sTs;
    2.30 +    val (cts,tye2) = Thm.read_def_cterms(thy,types,sorts) used false sTs;
    2.31      fun mkcVar(ixn,T) =
    2.32          let val U = typ_subst_TVars tye2 T
    2.33          in cterm_of thy (Var(ixn,U)) end
    2.34 @@ -573,7 +573,7 @@
    2.35  
    2.36  (*** Meta-Rewriting Rules ***)
    2.37  
    2.38 -fun read_prop s = read_cterm ProtoPure.thy (s, propT);
    2.39 +fun read_prop s = Thm.read_cterm ProtoPure.thy (s, propT);
    2.40  
    2.41  fun store_thm name thm = hd (PureThy.smart_store_thms (name, [thm]));
    2.42  fun store_standard_thm name thm = store_thm name (standard thm);