# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 7c652e4a924a060d548700214cefa5064070b4de
# Parent  8fdfa9c4e7eda6528c635a15a0740b3b46286cd2
tuned

diff -r 8fdfa9c4e7ed -r 7c652e4a924a src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Dec 03 08:40:46 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -596,7 +596,7 @@
 
 val inductive_simps = gen_inductive_simps Attrib.intern_src Syntax.read_prop;
 val inductive_simps_i = gen_inductive_simps (K I) Syntax.check_prop;
-    
+
 (* prove induction rule *)
 
 fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono