Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thm.first_order_match;
authorwenzelm
Thu, 10 May 2007 00:39:46 +0200
changeset 22901 481cd919c47f
parent 22900 f8a7c10e1bd0
child 22902 ac833b4bb7ee
Thm.first_order_match;
src/HOL/Nominal/nominal_inductive.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle