Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nominal/nominal_induct.ML
changeset 59058 a78612c67ec0
parent 58957 c9e744ea8a38
child 59580 cbc38731d42f 
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Nov 26 16:55:43 2014 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Nov 26 20:05:34 2014 +0100
@@ -54,7 +54,7 @@
       end;
      val substs =
        map2 subst insts concls |> flat |> distinct (op =)
-       |> map (pairself (Thm.cterm_of (Proof_Context.theory_of ctxt)));
+       |> map (apply2 (Thm.cterm_of (Proof_Context.theory_of ctxt)));
   in 
     (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
   end;
isabelle