TypeInfer.logicT;
authorwenzelm
Wed Jan 05 11:35:18 2000 +0100 (2000-01-05)
changeset 808678e254305ae6
parent 8085 dce06445aafd
child 8087 4187ef29d826
TypeInfer.logicT;
src/Pure/drule.ML
src/Pure/goals.ML
     1.1 --- a/src/Pure/drule.ML	Tue Jan 04 17:05:43 2000 +0100
     1.2 +++ b/src/Pure/drule.ML	Wed Jan 05 11:35:18 2000 +0100
     1.3 @@ -566,7 +566,7 @@
     1.4  val triv_forall_equality =
     1.5    let val V  = read_prop "PROP V"
     1.6        and QV = read_prop "!!x::'a. PROP V"
     1.7 -      and x  = read_cterm proto_sign ("x", TFree("'a",logicS));
     1.8 +      and x  = read_cterm proto_sign ("x", TypeInfer.logicT);
     1.9    in
    1.10      store_thm "triv_forall_equality"
    1.11        (equal_intr (implies_intr QV (forall_elim x (assume QV)))
     2.1 --- a/src/Pure/goals.ML	Tue Jan 04 17:05:43 2000 +0100
     2.2 +++ b/src/Pure/goals.ML	Wed Jan 05 11:35:18 2000 +0100
     2.3 @@ -541,8 +541,7 @@
     2.4  
     2.5  fun top_sg() = #sign(rep_thm(topthm()));
     2.6  
     2.7 -fun read s = term_of (read_cterm (top_sg())
     2.8 -			                   (s, (TVar(("DUMMY",0),[]))));
     2.9 +fun read s = term_of (read_cterm (top_sg()) (s, TypeInfer.logicT));
    2.10  
    2.11  (*Print a term under the current signature of the proof state*)
    2.12  fun prin t = writeln (Sign.string_of_term (top_sg()) t);