# HG changeset patch
# User wenzelm
# Date 1238336024 -7200
# Node ID 5daee9354a9c6743ba1860938cc12d9416d27120
# Parent  6cc9964436c3807846836a29626a8731d122a3bf
unified binding prefix terminology;

diff -r 6cc9964436c3 -r 5daee9354a9c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Mar 29 16:13:24 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Mar 29 16:13:44 2009 +0200
@@ -158,7 +158,7 @@
 
 (* Instantiation morphism *)
 
-fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt =
+fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
   let
     (* parameters *)
     val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
@@ -179,7 +179,7 @@
     val inst = Symtab.make insts'';
   in
     (Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
-      Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
+      Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
   end;