# HG changeset patch
# User wenzelm
# Date 1322086079 -3600
# Node ID 5296df35b656919af05a55295c614108b4c1cf01
# Parent  f2a587696afbc7b1254696d6dbbe60605df052b0
tuned;

diff -r f2a587696afb -r 5296df35b656 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Wed Nov 23 22:59:39 2011 +0100
+++ b/src/Pure/raw_simplifier.ML	Wed Nov 23 23:07:59 2011 +0100
@@ -576,10 +576,10 @@
 fun add_eqcong thm ss = ss |>
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     let
-      val (lhs, _) = Thm.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
+      val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
     (*val lhs = Envir.eta_contract lhs;*)
-      val a = the (cong_name (head_of (term_of lhs))) handle Option.Option =>
+      val a = the (cong_name (head_of lhs)) handle Option.Option =>
         raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
       val (xs, weak) = congs;
       val _ =
@@ -593,8 +593,8 @@
 fun del_eqcong thm ss = ss |>
   map_simpset2 (fn (congs, procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) =>
     let
-      val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
-        raise SIMPLIFIER ("Congruence not a meta-equality", thm);
+      val (lhs, _) = Logic.dest_equals (Thm.concl_of thm)
+        handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
     (*val lhs = Envir.eta_contract lhs;*)
       val a = the (cong_name (head_of lhs)) handle Option.Option =>
         raise SIMPLIFIER ("Congruence must start with a constant", thm);