--- 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
--- 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}