# HG changeset patch
# User wenzelm
# Date 1284989393 -7200
# Node ID 32a00ff29d1a0a5833784abdceb868e62adaae8c
# Parent  ccb223a4d49c8404fb79eabc03bbe11ebc416528
more antiquotations;

diff -r ccb223a4d49c -r 32a00ff29d1a src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Sep 20 15:08:51 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon Sep 20 15:29:53 2010 +0200
@@ -3340,7 +3340,7 @@
     (Object_Logic.judgment_conv (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt))
     THEN' rtac TrueI
 
-  val form_equations = PureThy.get_thms @{theory} "interpret_form_equations";
+  val form_equations = @{thms interpret_form_equations};
 
   fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
       fun lookup_splitting (Free (name, typ))