# HG changeset patch
# User krauss
# Date 1288088341 -7200
# Node ID 11ea439d947f23ca85f9dd30b47a8a8d6a7a667f
# Parent  d3bc972b7d9d19fee48fca20a3967df0459eed7e
declare recursive equation as ".simps", in accordance with other packages

diff -r d3bc972b7d9d -r 11ea439d947f src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Tue Oct 26 12:19:01 2010 +0200
@@ -218,7 +218,7 @@
     lthy'
     |> Local_Theory.note (eq_abinding, [rec_rule])
     |-> (fn (_, rec') =>
-      Local_Theory.note ((Binding.qualify true fname (Binding.name "rec"), []), rec'))
+      Local_Theory.note ((Binding.qualify true fname (Binding.name "simps"), []), rec'))
     |> snd
   end;
 
diff -r d3bc972b7d9d -r 11ea439d947f src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Tue Oct 26 11:51:09 2010 +0200
+++ b/src/HOL/ex/Fundefs.thy	Tue Oct 26 12:19:01 2010 +0200
@@ -222,7 +222,7 @@
      then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
      else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
 
-declare collatz.rec[code]
+declare collatz.simps[code]
 value "collatz 23"