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.
unified binding prefix terminology;
authorwenzelm
Sun, 29 Mar 2009 16:13:44 +0200
changeset 30774 5daee9354a9c
parent 30773 6cc9964436c3
child 30775 71f777103225
unified binding prefix terminology;
src/Pure/Isar/expression.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle