src/HOL/Import/shuffler.ML
changeset 17440 df77edc4f5d0
parent 17188 a26a4fc323ed
child 17463 e9c1574d0caf
     1.1 --- a/src/HOL/Import/shuffler.ML	Fri Sep 16 20:30:44 2005 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Fri Sep 16 21:02:15 2005 +0200
     1.3 @@ -343,9 +343,9 @@
     1.4  		       SOME res
     1.5  		  end
     1.6  	      else NONE)
     1.7 -	     handle e => (writeln "eta_contract:";print_exn e))
     1.8 -	  | _ => (error ("Bad eta_contract argument" ^ (string_of_cterm (cterm_of sg t))); NONE)
     1.9 -    end
    1.10 +	     handle e => print_exn e)
    1.11 +	  | _ => NONE
    1.12 +       end
    1.13  
    1.14  fun beta_fun sg assume t =
    1.15      SOME (beta_conversion true (cterm_of sg t))
    1.16 @@ -486,6 +486,7 @@
    1.17  be handy in its own right, for example for indexing terms. *)
    1.18  
    1.19  fun norm_term thy t =
    1.20 +    PolyML.exception_trace (fn () =>
    1.21      let
    1.22  	val sg = sign_of thy
    1.23  
    1.24 @@ -494,8 +495,8 @@
    1.25  			  addsimps (map (Thm.transfer sg) norms)
    1.26  	fun chain f th =
    1.27  	    let
    1.28 -		val rhs = snd (dest_equals (cprop_of th))
    1.29 -	    in
    1.30 +                val rhs = snd (dest_equals (cprop_of th))
    1.31 +      	    in
    1.32  		transitive th (f rhs)
    1.33  	    end
    1.34  
    1.35 @@ -508,7 +509,7 @@
    1.36  	val _ = message ("norm_term: " ^ (string_of_thm th))
    1.37      in
    1.38  	th
    1.39 -    end
    1.40 +    end)
    1.41      handle e => (writeln "norm_term internal error"; print_sign_exn (sign_of thy) e)
    1.42  
    1.43