# HG changeset patch
# User krauss
# Date 1296632865 -3600
# Node ID d8efc2490b8e3ffac062879fc07322eb6d2941b9
# Parent  e29ea98a76ce603f8c7d9aa7cb4aec99c19908cb
made SML/NJ happy

diff -r e29ea98a76ce -r d8efc2490b8e src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Tue Feb 01 21:09:52 2011 +0100
+++ b/src/Pure/Thy/term_style.ML	Wed Feb 02 08:47:45 2011 +0100
@@ -110,14 +110,12 @@
   | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
   | isub_term t = t;
 
-val style_isub = Scan.succeed (K isub_term);
-
 val _ = Context.>> (Context.map_theory
  (setup "lhs" (style_lhs_rhs fst) #>
   setup "rhs" (style_lhs_rhs snd) #>
   setup "prem" style_prem #>
   setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
-  setup "isub" style_isub #>
+  setup "isub" (Scan.succeed (K isub_term)) #>
   setup "prem1" (style_parm_premise 1) #>
   setup "prem2" (style_parm_premise 2) #>
   setup "prem3" (style_parm_premise 3) #>