--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Oct 30 09:55:15 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Oct 31 10:02:37 2009 +0100
@@ -126,8 +126,9 @@
|> split_all_pairs thy
|> tap check_equation_format
-fun inline_equations thy th = Conv.fconv_rule (Simplifier.rewrite
-((Simplifier.theory_context thy Simplifier.empty_ss) addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
+fun inline_equations thy th = Conv.fconv_rule
+ (Simplifier.rewrite ((Simplifier.theory_context thy Simplifier.empty_ss)
+ addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th
fun store_thm_in_table ignore_consts thy th=
let