# HG changeset patch
# User wenzelm
# Date 1169422829 -3600
# Node ID d0926c4ea65362873152537851c764accd896cb4
# Parent  47b36483f872d5f61b14c2842a31c539a28e4ab0
tuned;

diff -r 47b36483f872 -r d0926c4ea653 src/HOL/ex/Binary.thy
--- 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);