# HG changeset patch
# User wenzelm
# Date 979314980 -3600
# Node ID f6b16554720d456d9678924d46bc3683c7056c3e
# Parent  90695f46440b170abd4a675b8da0ea2508145aa2
made SML/NJ happy;

diff -r 90695f46440b -r f6b16554720d src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Fri Jan 12 16:32:01 2001 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Fri Jan 12 16:56:20 2001 +0100
@@ -96,8 +96,8 @@
 
 in
 
-val make = gen_make false;
-val make_raw = gen_make true;
+fun make x = gen_make false x;
+fun make_raw x = gen_make true x;
 
 end;