src/HOL/Tools/refute_isar.ML
changeset 14454 8a8330bef1f8
parent 14350 41b32020d0b3
child 15570 8d8c70b41bab
     1.1 --- a/src/HOL/Tools/refute_isar.ML	Wed Mar 10 20:28:18 2004 +0100
     1.2 +++ b/src/HOL/Tools/refute_isar.ML	Wed Mar 10 20:31:47 2004 +0100
     1.3 @@ -74,8 +74,8 @@
     1.4  
     1.5  	fun refute_params_trans args =
     1.6  		let
     1.7 -			fun add_params (thy, []) = thy
     1.8 -				| add_params (thy, p::ps) = add_params (Refute.set_default_param p thy, ps)
     1.9 +			fun add_params (thy, [])    = thy
    1.10 +			  | add_params (thy, p::ps) = add_params (Refute.set_default_param p thy, ps)
    1.11  		in
    1.12  			Toplevel.theory (fn thy =>
    1.13  				let