--- a/src/HOL/Decision_Procs/approximation.ML Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Wed Apr 08 19:39:08 2015 +0200
@@ -50,7 +50,7 @@
(* Should be in HOL.thy ? *)
fun gen_eval_tac conv ctxt = CONVERSION
- (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
+ (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
THEN' rtac TrueI
val form_equations = @{thms interpret_form_equations};