added explicit check phase after reading of specification
authorhaftmann
Tue Apr 22 08:33:23 2008 +0200 (2008-04-22)
changeset 26736e6091328718f
parent 26735 39be3c7e643a
child 26737 3d46c55f03af
added explicit check phase after reading of specification
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Apr 22 08:33:21 2008 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Apr 22 08:33:23 2008 +0200
     1.3 @@ -822,7 +822,7 @@
     1.4              member (op =) ps t then I else insert (op =) v
     1.5          | _ => I) r []), r);
     1.6  
     1.7 -    val intros = map (apsnd (close_rule #> expand)) pre_intros;
     1.8 +    val intros = map (apsnd (Syntax.check_term lthy #> close_rule #> expand)) pre_intros;
     1.9      val preds = map (fn ((c, _), mx) => (c, mx)) cnames_syn';
    1.10    in
    1.11      lthy