made SML/NJ happy;
authorwenzelm
Tue Dec 31 11:19:14 2013 +0100 (2013-12-31)
changeset 5488261276a7fc369
parent 54881 dff57132cf18
child 54883 dd04a8b654fc
made SML/NJ happy;
src/Pure/Isar/class_declaration.ML
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Mon Dec 30 20:35:17 2013 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Tue Dec 31 11:19:14 2013 +0100
     1.3 @@ -368,9 +368,11 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val subclass = gen_subclass (K I) user_proof;
     1.8  fun prove_subclass before_exit tac = gen_subclass (K I) (tactic_proof tac) before_exit;
     1.9 -val subclass_cmd = gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof;
    1.10 +
    1.11 +fun subclass x = gen_subclass (K I) user_proof x;
    1.12 +fun subclass_cmd x =
    1.13 +  gen_subclass (Proof_Context.read_class o Proof_Context.init_global) user_proof x;
    1.14  
    1.15  end; (*local*)
    1.16