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.
removed ProofContext.declare_thm;
authorwenzelm
Thu, 30 Sep 1999 23:31:13 +0200
changeset 7668 80c310e76c46
parent 7667 22dc8b2455b8
child 7669 fcd9c2050836
removed ProofContext.declare_thm;
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/attrib.ML	Thu Sep 30 21:23:08 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Sep 30 23:31:13 1999 +0200
@@ -214,7 +214,7 @@
     val (xs, ss) = Library.split_list insts;
     val Ts = map get_typ xs;
 
-    val (ts, envT) = ProofContext.read_termTs (ctxt |> ProofContext.declare_thm thm) (ss ~~ Ts);
+    val (ts, envT) = ProofContext.read_termTs ctxt (ss ~~ Ts);
     val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
     val cenv =
       map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
isabelle