src/Pure/Proof/extraction.ML
changeset 19391 4812d28c90a6
parent 19305 5c16895d548b
child 19466 29bc35832a77
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Apr 09 19:41:30 2006 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Apr 10 00:33:49 2006 +0200
     1.3 @@ -49,7 +49,7 @@
     1.4  val nullt = Const ("Null", nullT);
     1.5  
     1.6  fun mk_typ T =
     1.7 -  Const ("Type", itselfT T --> Type ("Type", [])) $ Logic.mk_type T;
     1.8 +  Const ("Type", Term.itselfT T --> Type ("Type", [])) $ Logic.mk_type T;
     1.9  
    1.10  fun typeof_proc defaultS vs (Const ("typeof", _) $ u) =
    1.11        SOME (mk_typ (case strip_comb u of