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.
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
authorhaftmann
Mon, 15 Feb 2010 14:04:06 +0100
changeset 35127 5b29c1660047
parent 35126 ce6544f42eb9
child 35128 c1ad622e90e4
child 35156 37872c68a385
apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
src/Pure/Isar/theory_target.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/theory_target.ML	Mon Feb 15 14:04:06 2010 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Feb 15 14:04:06 2010 +0100
@@ -88,7 +88,7 @@
   in
     if target = "" then
       lthy
-      |> direct_decl target_decl
+      |> direct_decl global_decl
     else
       lthy
       |> pervasive ? direct_decl global_decl
isabelle