src/HOL/Import/shuffler.ML
changeset 17959 8db36a108213
parent 17892 62c397c17d18
child 18127 9f03d8a9a81b
     1.1 --- a/src/HOL/Import/shuffler.ML	Fri Oct 21 18:14:37 2005 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Fri Oct 21 18:14:38 2005 +0200
     1.3 @@ -223,7 +223,7 @@
     1.4  	val rew = Logic.mk_equals (lhs,rhs)
     1.5  	val init = trivial (cterm_of sg rew)
     1.6      in
     1.7 -	(all_comm RS init handle e => (message "rew_th"; print_exn e))
     1.8 +	(all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
     1.9      end
    1.10  
    1.11  fun quant_rewrite sg assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
    1.12 @@ -343,7 +343,7 @@
    1.13  		       SOME res
    1.14  		  end
    1.15  	      else NONE)
    1.16 -	     handle e => print_exn e)
    1.17 +	     handle e => OldGoals.print_exn e)
    1.18  	  | _ => NONE
    1.19         end
    1.20  
    1.21 @@ -411,7 +411,7 @@
    1.22  	    else NONE
    1.23  	  | _ => (error ("Bad eta_expand argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
    1.24      end
    1.25 -    handle e => (writeln "eta_expand internal error";print_exn e)
    1.26 +    handle e => (writeln "eta_expand internal error"; OldGoals.print_exn e)
    1.27  
    1.28  fun mk_tfree s = TFree("'"^s,[])
    1.29  val xT = mk_tfree "a"
    1.30 @@ -524,7 +524,7 @@
    1.31      in
    1.32  	Drule.forall_intr_list (map (cterm_of sg) vars) th
    1.33      end
    1.34 -    handle e => (writeln "close_thm internal error"; print_exn e)
    1.35 +    handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
    1.36  
    1.37  (* Normalizes a theorem's conclusion using norm_term. *)
    1.38  
    1.39 @@ -622,7 +622,7 @@
    1.40  					else error "Internal error in set_prop"
    1.41  	     | NONE => NONE
    1.42      end
    1.43 -    handle e => (writeln "set_prop internal error"; print_exn e)
    1.44 +    handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
    1.45  
    1.46  fun find_potential thy t =
    1.47      let