src/HOL/Import/shuffler.ML
changeset 37778 87b5dfe00387
parent 37146 f652333bbf8e
child 38549 d0385f2764d8
     1.1 --- a/src/HOL/Import/shuffler.ML	Mon Jul 12 18:59:38 2010 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Mon Jul 12 20:21:39 2010 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4          val rew = Logic.mk_equals (lhs,rhs)
     1.5          val init = Thm.trivial (cterm_of thy rew)
     1.6      in
     1.7 -        (all_comm RS init handle e => (message "rew_th"; OldGoals.print_exn e))
     1.8 +        all_comm RS init
     1.9      end
    1.10  
    1.11  fun quant_rewrite thy assumes (t as Const("all",T1) $ (Abs(x,xT,Const("all",T2) $ Abs(y,yT,body)))) =
    1.12 @@ -315,7 +315,7 @@
    1.13      in
    1.14          case t of
    1.15              Const("all",_) $ (Abs(x,xT,Const("==",eqT) $ P $ Q)) =>
    1.16 -            ((if eta_redex P andalso eta_redex Q
    1.17 +            (if eta_redex P andalso eta_redex Q
    1.18                then
    1.19                    let
    1.20                        val cert = cterm_of thy
    1.21 @@ -340,7 +340,6 @@
    1.22                         SOME res
    1.23                    end
    1.24                else NONE)
    1.25 -             handle e => OldGoals.print_exn e)
    1.26            | _ => NONE
    1.27         end
    1.28  
    1.29 @@ -521,7 +520,7 @@
    1.30      in
    1.31          Drule.forall_intr_list (map (cterm_of thy) vars) th
    1.32      end
    1.33 -    handle e => (writeln "close_thm internal error"; OldGoals.print_exn e)
    1.34 +
    1.35  
    1.36  (* Normalizes a theorem's conclusion using norm_term. *)
    1.37  
    1.38 @@ -618,7 +617,6 @@
    1.39                                          else error "Internal error in set_prop"
    1.40               | NONE => NONE
    1.41      end
    1.42 -    handle e => (writeln "set_prop internal error"; OldGoals.print_exn e)
    1.43  
    1.44  fun find_potential thy t =
    1.45      let