# HG changeset patch
# User wenzelm
# Date 1165768675 -3600
# Node ID 5b76448793734020c114ba4161b475c73fc77c09
# Parent  39b2ce38ac66fa208a00340d6a316ab5b545b8f9
removed junk;

diff -r 39b2ce38ac66 -r 5b7644879373 src/Pure/Isar/proof_context.ML
--- 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 *)
diff -r 39b2ce38ac66 -r 5b7644879373 src/Pure/Isar/theory_target.ML
--- 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;