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.
src/CCL/Term.thy
changeset 26342 0f65fa163304
parent 24825 c4f13ab78f9d
child 26480 544cef16045b 
--- a/src/CCL/Term.thy	Wed Mar 19 22:47:39 2008 +0100
+++ b/src/CCL/Term.thy	Wed Mar 19 22:50:42 2008 +0100
@@ -209,11 +209,11 @@
 
 fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
            (fn _ => [stac letrecB 1,
-                     simp_tac (simpset () addsimps rawBs) 1]);
+                     simp_tac (@{simpset} addsimps rawBs) 1]);
 fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
 
 fun raw_mk_beta_rl defs s = prove_goalw (the_context ()) defs s
-           (fn _ => [simp_tac (simpset () addsimps rawBs
+           (fn _ => [simp_tac (@{simpset} addsimps rawBs
                                setloop (stac letrecB)) 1]);
 fun mk_beta_rl s = raw_mk_beta_rl data_defs s;
 
@@ -298,7 +298,7 @@
 
 local
   fun mk_thm s = prove_goalw (the_context ()) (thms "data_defs") s (fn _ =>
-    [simp_tac (simpset () addsimps (thms "ccl_porews")) 1])
+    [simp_tac (@{simpset} addsimps (thms "ccl_porews")) 1])
 in
   val term_porews = map mk_thm ["inl(a) [= inl(a') <-> a [= a'",
                                 "inr(b) [= inr(b') <-> b [= b'",
isabelle