--- a/src/HOL/Complex/ex/MIR.thy Wed Sep 17 21:27:14 2008 +0200
+++ b/src/HOL/Complex/ex/MIR.thy Wed Sep 17 21:27:17 2008 +0200
@@ -5819,7 +5819,7 @@
@{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
| num_of_term vs (@{term "number_of :: int \<Rightarrow> real"} $ t') =
@{code C} (HOLogic.dest_numeral t')
- | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
+ | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
fun fm_of_term vs @{term True} = @{code T}
| fm_of_term vs @{term False} = @{code F}
@@ -5845,7 +5845,7 @@
@{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
| fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
- | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
+ | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i
| term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy Wed Sep 17 21:27:14 2008 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy Wed Sep 17 21:27:17 2008 +0200
@@ -2016,7 +2016,7 @@
| _ => error "num_of_term: unsupported Multiplication")
| num_of_term vs (@{term "real :: int \<Rightarrow> real"} $ (@{term "number_of :: int \<Rightarrow> int"} $ t')) = @{code C} (HOLogic.dest_numeral t')
| num_of_term vs (@{term "number_of :: int \<Rightarrow> real"} $ t') = @{code C} (HOLogic.dest_numeral t')
- | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
+ | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
fun fm_of_term vs @{term True} = @{code T}
| fm_of_term vs @{term False} = @{code F}
@@ -2032,7 +2032,7 @@
@{code E} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
| fm_of_term vs (Const ("All", _) $ Abs (xn, xT, p)) =
@{code A} (fm_of_term (map (fn (v, n) => (v, n + 1)) vs) p)
- | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
+ | fm_of_term vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
fun term_of_num vs (@{code C} i) = @{term "real :: int \<Rightarrow> real"} $ HOLogic.mk_number HOLogic.intT i
| term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))
--- a/src/HOL/ex/Reflected_Presburger.thy Wed Sep 17 21:27:14 2008 +0200
+++ b/src/HOL/ex/Reflected_Presburger.thy Wed Sep 17 21:27:17 2008 +0200
@@ -1941,7 +1941,7 @@
| NONE => (case try HOLogic.dest_number t2
of SOME (_, i) => @{code Mul} (i, num_of_term vs t1)
| NONE => error "num_of_term: unsupported multiplication"))
- | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term_global @{theory} t);
+ | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term @{context} t);
fun fm_of_term ps vs @{term True} = @{code T}
| fm_of_term ps vs @{term False} = @{code F}
@@ -1975,7 +1975,7 @@
val (xn', p') = variant_abs (xn, xT, p);
val vs' = (Free (xn', xT), 0) :: map (fn (v, n) => (v, n + 1)) vs;
in @{code A} (fm_of_term ps vs' p) end
- | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term_global @{theory} t);
+ | fm_of_term ps vs t = error ("fm_of_term : unknown term " ^ Syntax.string_of_term @{context} t);
fun term_of_num vs (@{code C} i) = HOLogic.mk_number HOLogic.intT i
| term_of_num vs (@{code Bound} n) = fst (the (find_first (fn (_, m) => n = m) vs))