src/Pure/axclass.ML
changeset 36106 19deea200358
parent 35961 00e48e1d9afd
child 36325 8715343af626
--- a/src/Pure/axclass.ML	Sun Apr 11 14:06:35 2010 +0200
+++ b/src/Pure/axclass.ML	Sun Apr 11 14:30:34 2010 +0200
@@ -306,11 +306,11 @@
     |-> (fn const' as Const (c'', _) =>
       Thm.add_def false true
         (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
-      #>> Thm.varifyT_global
-      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
-      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
-      #> snd
-      #> pair (Const (c, T))))
+      #>> apsnd Thm.varifyT_global
+      #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
+        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
+        #> snd
+        #> pair (Const (c, T))))
     ||> Sign.restore_naming thy
   end;
 
@@ -325,7 +325,7 @@
   in
     thy
     |> Thm.add_def false false (b', prop)
-    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
+    |>> (fn (_, thm) =>  Drule.transitive_thm OF [eq, thm])
   end;
 
 
@@ -515,7 +515,7 @@
 
 fun add_axiom (b, prop) =
   Thm.add_axiom (b, prop) #->
-  (fn thm => PureThy.add_thm ((b, Drule.export_without_context thm), []));
+  (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
 
 fun axiomatize prep mk name add raw_args thy =
   let