src/Pure/Isar/expression.ML
changeset 37313 715d25555ca6
parent 37145 01aa36932739
child 38107 3a46cebd7983
equal deleted inserted replaced
37312:664d3110beb2 37313:715d25555ca6
   730 
   730 
   731     val ((fixed, deps, body_elems), (parms, ctxt')) =
   731     val ((fixed, deps, body_elems), (parms, ctxt')) =
   732       prep_decl raw_import I raw_body (ProofContext.init_global thy);
   732       prep_decl raw_import I raw_body (ProofContext.init_global thy);
   733     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
   733     val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems;
   734 
   734 
       
   735     val extraTs =
       
   736       subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
       
   737     val _ =
       
   738       if null extraTs then ()
       
   739       else warning ("Additional type variable(s) in locale specification " ^
       
   740         quote (Binding.str_of binding) ^ ": " ^
       
   741           commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
       
   742 
   735     val predicate_binding =
   743     val predicate_binding =
   736       if Binding.is_empty raw_predicate_binding then binding
   744       if Binding.is_empty raw_predicate_binding then binding
   737       else raw_predicate_binding;
   745       else raw_predicate_binding;
   738     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   746     val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') =
   739       define_preds predicate_binding parms text thy;
   747       define_preds predicate_binding parms text thy;
   740 
       
   741     val extraTs = subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []);
       
   742     val _ =
       
   743       if null extraTs then ()
       
   744       else warning ("Additional type variable(s) in locale specification " ^
       
   745         quote (Binding.str_of binding));
       
   746 
   748 
   747     val a_satisfy = Element.satisfy_morphism a_axioms;
   749     val a_satisfy = Element.satisfy_morphism a_axioms;
   748     val b_satisfy = Element.satisfy_morphism b_axioms;
   750     val b_satisfy = Element.satisfy_morphism b_axioms;
   749 
   751 
   750     val params = fixed @
   752     val params = fixed @