# HG changeset patch
# User wenzelm
# Date 1204377013 -3600
# Node ID 3e099fc47afd61953f3784c18e18a076f578a7ef
# Parent  9af968b694d94aa96992b9a54ca33e2cdb2242f5
use more antiquotations;

diff -r 9af968b694d9 -r 3e099fc47afd src/HOL/SizeChange/sct.ML
--- a/src/HOL/SizeChange/sct.ML	Thu Feb 28 18:59:22 2008 +0100
+++ b/src/HOL/SizeChange/sct.ML	Sat Mar 01 14:10:13 2008 +0100
@@ -63,9 +63,6 @@
     in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end
 
 
-val less_nat_const = Const (@{const_name HOL.less}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-val lesseq_nat_const = Const (@{const_name HOL.less_eq}, HOLogic.natT --> HOLogic.natT --> HOLogic.boolT)
-
 val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"]
 
 val all_less_zero = thm "Interpretation.all_less_zero"
@@ -232,11 +229,11 @@
                                       |> CLASIMPSET auto_tac |> Seq.hd
 
                       val decr = forall_intr (cterm_of thy relvar)
-                                   #> forall_elim (cterm_of thy less_nat_const)
+                                   #> forall_elim (cterm_of thy @{const HOL.less(nat)})
                                    #> CLASIMPSET auto_tac #> Seq.hd
 
                       val decreq = forall_intr (cterm_of thy relvar)
-                                     #> forall_elim (cterm_of thy lesseq_nat_const)
+                                     #> forall_elim (cterm_of thy @{const HOL.less_eq(nat)})
                                      #> CLASIMPSET auto_tac #> Seq.hd
 
                       val thm1 = decr with_m2
diff -r 9af968b694d9 -r 3e099fc47afd src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Thu Feb 28 18:59:22 2008 +0100
+++ b/src/HOL/ex/Binary.thy	Sat Mar 01 14:10:13 2008 +0100
@@ -23,13 +23,13 @@
 ML {*
 structure Binary =
 struct
-  fun dest_bit (Const ("False", _)) = 0
-    | dest_bit (Const ("True", _)) = 1
+  fun dest_bit (Const (@{const_name False}, _)) = 0
+    | dest_bit (Const (@{const_name True}, _)) = 1
     | dest_bit t = raise TERM ("dest_bit", [t]);
 
-  fun dest_binary (Const (@{const_name HOL.zero}, Type ("nat", _))) = 0
-    | dest_binary (Const (@{const_name HOL.one}, Type ("nat", _))) = 1
-    | dest_binary (Const ("Binary.bit", _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
+  fun dest_binary (Const (@{const_name HOL.zero}, Type (@{type_name nat}, _))) = 0
+    | dest_binary (Const (@{const_name HOL.one}, Type (@{type_name nat}, _))) = 1
+    | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
     | dest_binary t = raise TERM ("dest_binary", [t]);
 
   fun mk_bit 0 = @{term False}