# HG changeset patch
# User bulwahn
# Date 1257491518 -3600
# Node ID 767cfb37833ea058e5a489f41c229d15ce96c0b3
# Parent  3b275a0bf18c23edb7a799404417399f3e2c598f
made SML/NJ happy; tuned

diff -r 3b275a0bf18c -r 767cfb37833e src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -2074,7 +2074,7 @@
     (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t
   | (c as Const (@{const_name Not}, _), [t]) => (case dest_prem thy params t of          
       Prem (ts, t) => Negprem (ts, t)
-    | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) 
+    | Negprem _ => error ("Double negation not allowed in premise: " ^ Syntax.string_of_term_global thy (c $ t)) 
     | Sidecond t => Sidecond (c $ t))
   | (c as Const (s, _), ts) =>
     if is_registered thy s then
@@ -2206,7 +2206,7 @@
             val eq_term = HOLogic.mk_Trueprop
               (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
             val def = predfun_definition_of thy predname full_mode
-            val tac = fn {...} => Simplifier.simp_tac
+            val tac = fn _ => Simplifier.simp_tac
               (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1
             val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac
           in
@@ -2506,7 +2506,7 @@
         NONE => (if random then [@{term "5 :: code_numeral"}] else [])
       | SOME d => [@{term "True"}, HOLogic.mk_number @{typ "code_numeral"} d]
     val comp_modifiers =
-      case depth_limit of NONE => 
+      case depth_limit of NONE =>
       (if random then random_comp_modifiers else
        if annotated then annotated_comp_modifiers else predicate_comp_modifiers) | SOME _ => depth_limited_comp_modifiers
     val mk_fun_of =
diff -r 3b275a0bf18c -r 767cfb37833e src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Nov 06 08:11:58 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Fri Nov 06 08:11:58 2009 +0100
@@ -161,7 +161,9 @@
 
 fun make_const_spec_table options thy =
   let
-    fun store ignore_const f = fold (store_thm_in_table options ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
+    fun store ignore_const f =
+      fold (store_thm_in_table options ignore_const thy)
+        (map (Thm.transfer thy) (f (ProofContext.init thy)))
     val table = Symtab.empty
       |> store [] Predicate_Compile_Alternative_Defs.get
     val ignore_consts = Symtab.keys table