src/Pure/raw_simplifier.ML
changeset 61095 50e793295ce1
parent 61090 16f7f9aa4263
child 61098 e1b4b24f2ebd
     1.1 --- a/src/Pure/raw_simplifier.ML	Wed Sep 02 22:02:31 2015 +0200
     1.2 +++ b/src/Pure/raw_simplifier.ML	Wed Sep 02 22:14:44 2015 +0200
     1.3 @@ -640,7 +640,7 @@
     1.4        val a = the (cong_name (head_of lhs)) handle Option.Option =>
     1.5          raise SIMPLIFIER ("Congruence must start with a constant or free variable", [thm]);
     1.6        val (xs, weak) = congs;
     1.7 -      val xs' = AList.update (op =) (a, thm) xs;
     1.8 +      val xs' = AList.update (op =) (a, Thm.trim_context thm) xs;
     1.9        val weak' = if is_full_cong thm then weak else a :: weak;
    1.10      in ((xs', weak'), procs, mk_rews, termless, subgoal_tac, loop_tacs, solvers) end);
    1.11  
    1.12 @@ -1148,7 +1148,7 @@
    1.13                      (case cong_name h of
    1.14                        SOME a =>
    1.15                          (case AList.lookup (op =) (fst congs) a of
    1.16 -                           NONE => appc ()
    1.17 +                          NONE => appc ()
    1.18                          | SOME cong =>
    1.19       (*post processing: some partial applications h t1 ... tj, j <= length ts,
    1.20         may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)