unified binding prefix terminology;
authorwenzelm
Sun Mar 29 16:13:44 2009 +0200 (2009-03-29)
changeset 307745daee9354a9c
parent 30773 6cc9964436c3
child 30775 71f777103225
unified binding prefix terminology;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 29 16:13:24 2009 +0200
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 29 16:13:44 2009 +0200
     1.3 @@ -158,7 +158,7 @@
     1.4  
     1.5  (* Instantiation morphism *)
     1.6  
     1.7 -fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt =
     1.8 +fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
     1.9    let
    1.10      (* parameters *)
    1.11      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
    1.12 @@ -179,7 +179,7 @@
    1.13      val inst = Symtab.make insts'';
    1.14    in
    1.15      (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
    1.16 -      Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
    1.17 +      Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
    1.18    end;
    1.19  
    1.20