# HG changeset patch
# User wenzelm
# Date 1221679637 -7200
# Node ID e1dae766c108d79622bda85d9873567c59105efb
# Parent  69eaa97e7e9613ce3f091f318d7ebd5b62f8c852
local @{context};

diff -r 69eaa97e7e96 -r e1dae766c108 src/HOL/Complex/ex/MIR.thy
--- 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))
diff -r 69eaa97e7e96 -r e1dae766c108 src/HOL/Complex/ex/ReflectedFerrack.thy
--- 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))
diff -r 69eaa97e7e96 -r e1dae766c108 src/HOL/ex/Reflected_Presburger.thy
--- 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))