author | wenzelm |
Tue, 11 Apr 2006 16:00:07 +0200 | |
changeset 19410 | 9aef73143169 |
parent 19409 | 28bf2447c180 |
child 19411 | 8e207f560240 |
--- a/src/Pure/Isar/isar_syn.ML Tue Apr 11 16:00:06 2006 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Apr 11 16:00:07 2006 +0200 @@ -93,7 +93,7 @@ OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl ((P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name - >> (Toplevel.theory o (snd oo uncurry AxClass.add_axclass))); + >> (fn (x, y) => Toplevel.theory (snd o AxClass.add_axclass x [] y))); (* types *)