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.
removed junk;
authorwenzelm
Sun, 10 Dec 2006 17:37:55 +0100
changeset 21752 5b7644879373
parent 21751 39b2ce38ac66
child 21753 83b6cc133b28
removed junk;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/theory_target.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/proof_context.ML	Sun Dec 10 15:30:54 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Dec 10 17:37:55 2006 +0100
@@ -916,7 +916,6 @@
     val c' = Morphism.name phi c;
     val rhs' = Morphism.term phi rhs;
     val arg' = (c', rhs');
-    val FIXME = PolyML.print arg';
   in
     Context.mapping_result (Sign.add_abbrev mode arg') (add_abbrev mode arg')
     (* FIXME equiv_term *)
--- a/src/Pure/Isar/theory_target.ML	Sun Dec 10 15:30:54 2006 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Dec 10 17:37:55 2006 +0100
@@ -91,7 +91,7 @@
   in
     lthy1
     |> LocalTheory.theory (Sign.add_notation prmode [(v', mx')])
-    |> is_loc ? internal_abbrev (PolyML.print ((c, mx), Term.list_comb (v, xs)))
+    |> is_loc ? internal_abbrev ((c, mx), Term.list_comb (v, xs))
   end;
isabelle