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/Tools/transfer.ML
changeset 46497 89ccf66aa73d
parent 45620 f2a587696afb 
--- a/src/HOL/Tools/transfer.ML	Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/transfer.ML	Wed Feb 15 23:19:30 2012 +0100
@@ -109,7 +109,7 @@
     val ([a, D], ctxt2) = ctxt1
       |> Variable.import true (map Drule.mk_term [raw_a, raw_D])
       |>> map Drule.dest_term o snd;
-    val transform = Thm.capply @{cterm "Trueprop"} o Thm.capply D;
+    val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
     val T = Thm.typ_of (Thm.ctyp_of_term a);
     val (aT, bT) = (Term.range_type T, Term.domain_type T);
     
@@ -124,7 +124,7 @@
     val c_vars = map (certify o Var) vars;
     val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
     val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
-    val c_exprs' = map (Thm.capply a) c_vars';
+    val c_exprs' = map (Thm.apply a) c_vars';
 
     (* transfer *)
     val (hyps, ctxt5) = ctxt4
isabelle