# HG changeset patch
# User wenzelm
# Date 1178750386 -7200
# Node ID 481cd919c47f43cbabbfb49d658c61599104d5e5
# Parent  f8a7c10e1bd03952688a6bde9fcda46edc2daaaa
Thm.first_order_match;

diff -r f8a7c10e1bd0 -r 481cd919c47f src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu May 10 00:39:45 2007 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu May 10 00:39:46 2007 +0200
@@ -242,7 +242,7 @@
                  val vc_compat_ths' = map (fn th =>
                    let
                      val th' = gprems1 MRS
-                       Thm.instantiate (Thm.cterm_first_order_match
+                       Thm.instantiate (Thm.first_order_match
                          (Conjunction.mk_conjunction_list (cprems_of th),
                           Conjunction.mk_conjunction_list (map cprop_of gprems1))) th;
                      val (bop, lhs, rhs) = (case concl_of th' of