src/HOL/Bali/Term.thy
changeset 27226 5a3e5e46d977
parent 26480 544cef16045b
child 32960 69916a850301
--- a/src/HOL/Bali/Term.thy	Mon Jun 16 17:54:35 2008 +0200
+++ b/src/HOL/Bali/Term.thy	Mon Jun 16 17:54:36 2008 +0200
@@ -266,7 +266,7 @@
   is_stmt :: "term \<Rightarrow> bool"
  "is_stmt t \<equiv> \<exists>c. t=In1r c"
 
-ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
+ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{context} @{thm is_stmt_def}) *}
 
 declare is_stmt_rews [simp]