src/Pure/axclass.ML
changeset 36106 19deea200358
parent 35961 00e48e1d9afd
child 36325 8715343af626
     1.1 --- a/src/Pure/axclass.ML	Sun Apr 11 14:06:35 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sun Apr 11 14:30:34 2010 +0200
     1.3 @@ -306,11 +306,11 @@
     1.4      |-> (fn const' as Const (c'', _) =>
     1.5        Thm.add_def false true
     1.6          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
     1.7 -      #>> Thm.varifyT_global
     1.8 -      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
     1.9 -      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    1.10 -      #> snd
    1.11 -      #> pair (Const (c, T))))
    1.12 +      #>> apsnd Thm.varifyT_global
    1.13 +      #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
    1.14 +        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    1.15 +        #> snd
    1.16 +        #> pair (Const (c, T))))
    1.17      ||> Sign.restore_naming thy
    1.18    end;
    1.19  
    1.20 @@ -325,7 +325,7 @@
    1.21    in
    1.22      thy
    1.23      |> Thm.add_def false false (b', prop)
    1.24 -    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
    1.25 +    |>> (fn (_, thm) =>  Drule.transitive_thm OF [eq, thm])
    1.26    end;
    1.27  
    1.28  
    1.29 @@ -515,7 +515,7 @@
    1.30  
    1.31  fun add_axiom (b, prop) =
    1.32    Thm.add_axiom (b, prop) #->
    1.33 -  (fn thm => PureThy.add_thm ((b, Drule.export_without_context thm), []));
    1.34 +  (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
    1.35  
    1.36  fun axiomatize prep mk name add raw_args thy =
    1.37    let