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.
added explicit check phase after reading of specification
authorhaftmann
Tue, 22 Apr 2008 08:33:23 +0200
changeset 26736 e6091328718f
parent 26735 39be3c7e643a
child 26737 3d46c55f03af
added explicit check phase after reading of specification
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_package.ML	Tue Apr 22 08:33:21 2008 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue Apr 22 08:33:23 2008 +0200
@@ -822,7 +822,7 @@
             member (op =) ps t then I else insert (op =) v
         | _ => I) r []), r);
 
-    val intros = map (apsnd (close_rule #> expand)) pre_intros;
+    val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros;
     val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn';
   in
     lthy
isabelle