--- a/src/Pure/Isar/class_declaration.ML Mon Dec 30 20:35:17 2013 +0100
+++ b/src/Pure/Isar/class_declaration.ML Tue Dec 31 11:19:14 2013 +0100
@@ -368,9 +368,11 @@
in
-val subclass = gen_subclass (K I) user_proof;
fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
-val subclass_cmd = gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof;
+
+fun subclass x = gen_subclass (K I) user_proof x;
+fun subclass_cmd x =
+ gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof x;
end; (*local*)