src/Pure/axclass.ML
changeset 18124 a310c78298f9
parent 17956 369e2af8ee45
child 18377 0e1d025d57b3
     1.1 --- a/src/Pure/axclass.ML	Tue Nov 08 10:43:15 2005 +0100
     1.2 +++ b/src/Pure/axclass.ML	Tue Nov 08 10:44:40 2005 +0100
     1.3 @@ -303,7 +303,7 @@
     1.4  
     1.5  fun gen_instance mk_prop add_thms inst thy = thy
     1.6    |> ProofContext.init
     1.7 -  |> Proof.theorem_i Drule.internalK NONE (K (fold add_thms)) NONE ("", [])
     1.8 +  |> Proof.theorem_i Drule.internalK NONE (fold add_thms) NONE ("", [])
     1.9      (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
    1.10  
    1.11  in