diff -r b2daa27fc0a7 -r e18574413bc4 src/HOL/SizeChange/Examples.thy
--- a/src/HOL/SizeChange/Examples.thy	Mon May 12 22:03:33 2008 +0200
+++ b/src/HOL/SizeChange/Examples.thy	Mon May 12 22:11:06 2008 +0200
@@ -22,7 +22,7 @@
   apply (rule SCT_on_relations)
   apply (tactic "Sct.abs_rel_tac") (* Build call descriptors *)
   apply (rule ext, rule ext, simp) (* Show that they are correct *)
-  apply (tactic "Sct.mk_call_graph") (* Build control graph *)
+  apply (tactic "Sct.mk_call_graph @{context}") (* Build control graph *)
   apply (rule SCT_Main)                 (* Apply main theorem *)
   apply (simp add:finite_acg_simps) (* show finiteness *)
   oops (*FIXME by eval*) (* Evaluate to true *)
@@ -39,7 +39,7 @@
   apply (rule SCT_on_relations)
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
-  apply (tactic "Sct.mk_call_graph")
+  apply (tactic "Sct.mk_call_graph @{context}")
   apply (rule SCT_Main)
   apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
   oops (* FIXME by eval *)
@@ -57,7 +57,7 @@
   apply (rule SCT_on_relations)
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
-  apply (tactic "Sct.mk_call_graph")
+  apply (tactic "Sct.mk_call_graph @{context}")
   apply (rule SCT_Main)
   apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
   oops (* FIXME by eval *)
@@ -75,7 +75,7 @@
   apply (rule SCT_on_relations)
   apply (tactic "Sct.abs_rel_tac") 
   apply (rule ext, rule ext, simp) 
-  apply (tactic "Sct.mk_call_graph")
+  apply (tactic "Sct.mk_call_graph @{context}")
   apply (rule SCT_Main)
   apply (simp add:finite_acg_ins finite_acg_empty finite_graph_def) (* show finiteness *)
   by (simp only:sctTest_simps cong: sctTest_congs)