src/FOLP/simp.ML
changeset 36945 9bec62c10714
parent 36692 54b64d4ad524
child 42284 326f57825e1a
     1.1 --- a/src/FOLP/simp.ML	Sat May 15 21:41:32 2010 +0200
     1.2 +++ b/src/FOLP/simp.ML	Sat May 15 21:50:05 2010 +0200
     1.3 @@ -431,7 +431,7 @@
     1.4        are represented by rules, generalized over their parameters*)
     1.5  fun add_asms(ss,thm,a,anet,ats,cs) =
     1.6      let val As = strip_varify(nth_subgoal i thm, a, []);
     1.7 -        val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
     1.8 +        val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As;
     1.9          val new_rws = maps mk_rew_rules thms;
    1.10          val rwrls = map mk_trans (maps mk_rew_rules thms);
    1.11          val anet' = fold_rev lhs_insert_thm rwrls anet;