Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/rules.ML
changeset 10918 9679326489cd
parent 10781 eedf2def44c1
child 11632 6fc8de600f58 
--- a/TFL/rules.ML	Tue Jan 16 00:38:59 2001 +0100
+++ b/TFL/rules.ML	Tue Jan 16 00:40:57 2001 +0100
@@ -665,7 +665,7 @@
 
 fun CONTEXT_REWRITE_RULE (func, G, cut_lemma, congs) th =
  let val globals = func::G
-     val pbeta_reduce = simpl_conv empty_ss [split RS eq_reflection];
+     val pbeta_reduce = simpl_conv empty_ss [split_conv RS eq_reflection];
      val tc_list = ref[]: term list ref
      val dummy = term_ref := []
      val dummy = thm_ref  := []
isabelle