src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy

--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Mar 04 19:53:18 2015 +0100
@@ -4156,7 +4156,7 @@
 
   fn (ctxt, alternative, ty, ps, ct) =>
     Proof_Context.cterm_of ctxt
-      (frpar_procedure alternative ty ps (term_of ct))
+      (frpar_procedure alternative ty ps (Thm.term_of ct))
 
 end
 *}