# 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;