# HG changeset patch
# User haftmann
# Date 1177060901 -7200
# Node ID e2b06bfe471a16d3471b37b7a0bcaf8f50fdd94c
# Parent  06165e40e7bd3532bd5cadc303fb075404440d7f
improved case unfolding

diff -r 06165e40e7bd -r e2b06bfe471a src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Fri Apr 20 11:21:40 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Fri Apr 20 11:21:41 2007 +0200
@@ -65,8 +65,12 @@
 qed
 
 lemma [code inline]:
-  "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
+  "nat_case = (\<lambda>f g n. if n = 0 then f else g (nat_of_int (int n - 1)))"
+proof rule+
+  fix f g n
+  show "nat_case f g n = (if n = 0 then f else g (nat_of_int (int n - 1)))"
   by (cases n) (simp_all add: nat_of_int_int)
+qed
 
 text {*
   Most standard arithmetic functions on natural numbers are implemented
@@ -368,14 +372,10 @@
 
 end; (*local*)
 
-local
-  val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq";
-  val eq_reflection = thm "eq_reflection";
-in fun lift_obj_eq f thy =
-  map (fn thm => thm RS meta_eq_to_obj_eq)
+fun lift_obj_eq f thy =
+  map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
   #> f thy
-  #> map (fn thm => thm RS eq_reflection)
-end
+  #> map (fn thm => thm RS @{thm eq_reflection});
 *}
 
 setup {*