# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1306384589 -7200
# Node ID 036a19936febb47f7eac3e5299ce779e5853601d
# Parent  1a6593bc494de663c4dd9d72f204896a41180fa4
updated to new Isabelle

diff -r 1a6593bc494d -r 036a19936feb Nominal/nominal_function_core.ML
--- a/Nominal/nominal_function_core.ML	Wed May 25 21:38:50 2011 +0200
+++ b/Nominal/nominal_function_core.ML	Thu May 26 06:36:29 2011 +0200
@@ -793,7 +793,7 @@
     Goal.init goal
     |> (SINGLE (resolve_tac [accI] 1)) |> the
     |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
-    |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
+    |> (SINGLE (auto_tac ctxt)) |> the
     |> Goal.conclude
     |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   end