# HG changeset patch
# User wenzelm
# Date 1388485154 -3600
# Node ID 61276a7fc3690e76b9d9f6f251b75c86600e8794
# Parent  dff57132cf184f77cd5ce04817fcfdd42c0c9d02
made SML/NJ happy;

diff -r dff57132cf18 -r 61276a7fc369 src/Pure/Isar/class_declaration.ML
--- 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*)