--- a/src/FOLP/simp.ML Sat May 15 21:41:32 2010 +0200
+++ b/src/FOLP/simp.ML Sat May 15 21:50:05 2010 +0200
@@ -431,7 +431,7 @@
are represented by rules, generalized over their parameters*)
fun add_asms(ss,thm,a,anet,ats,cs) =
let val As = strip_varify(nth_subgoal i thm, a, []);
- val thms = map (trivial o cterm_of(Thm.theory_of_thm thm)) As;
+ val thms = map (Thm.trivial o cterm_of(Thm.theory_of_thm thm)) As;
val new_rws = maps mk_rew_rules thms;
val rwrls = map mk_trans (maps mk_rew_rules thms);
val anet' = fold_rev lhs_insert_thm rwrls anet;