src/Pure/drule.ML
changeset 8086 78e254305ae6
parent 7898 d7e65a52acf9
child 8129 29e239c7b8c2
     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)))