# HG changeset patch
# User webertj
# Date 1078947107 -3600
# Node ID 8a8330bef1f88e8a1e48737c144aa5bc8d3347d1
# Parent  3397a69dfa4e5bed0f276f0a7ca8d9bbbe0295c3
*** empty log message ***

diff -r 3397a69dfa4e -r 8a8330bef1f8 src/HOL/Tools/refute_isar.ML
--- a/src/HOL/Tools/refute_isar.ML	Wed Mar 10 20:28:18 2004 +0100
+++ b/src/HOL/Tools/refute_isar.ML	Wed Mar 10 20:31:47 2004 +0100
@@ -74,8 +74,8 @@
 
 	fun refute_params_trans args =
 		let
-			fun add_params (thy, []) = thy
-				| add_params (thy, p::ps) = add_params (Refute.set_default_param p thy, ps)
+			fun add_params (thy, [])    = thy
+			  | add_params (thy, p::ps) = add_params (Refute.set_default_param p thy, ps)
 		in
 			Toplevel.theory (fn thy =>
 				let