--- a/src/HOL/ex/Binary.thy Sun Jan 21 19:09:38 2007 +0100
+++ b/src/HOL/ex/Binary.thy Mon Jan 22 00:40:29 2007 +0100
@@ -113,6 +113,8 @@
ML {*
local
val binary_ss = HOL_basic_ss addsimps @{thms binary_simps};
+ fun prove ctxt prop =
+ Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
infix ==;
val op == = Logic.mk_equals;
@@ -120,9 +122,6 @@
fun plus m n = @{term "plus :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
fun mult m n = @{term "times :: nat \<Rightarrow> nat \<Rightarrow> nat"} $ m $ n;
- fun prove ctxt prop =
- Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));
-
exception FAIL;
fun the_arg t = (t, dest_binary t handle TERM _ => raise FAIL);