# HG changeset patch
# User wenzelm
# Date 753355837 -3600
# Node ID 6b26ccac50fc5c4c0f43686585879d413073aa38
# Parent  fdc1c3424247bc9d114b088d6b3d857682f3dad4
fun parents: removed pp block (didn't have any effect)

diff -r fdc1c3424247 -r 6b26ccac50fc src/Pure/Syntax/extension.ML
--- a/src/Pure/Syntax/extension.ML	Sun Nov 14 15:14:30 1993 +0100
+++ b/src/Pure/Syntax/extension.ML	Mon Nov 15 10:30:37 1993 +0100
@@ -233,7 +233,7 @@
   let
     fun descend (from, to) = Mfix ("_", to --> from, "", [0], 0);
 
-    fun parents T = Mfix ("(1'(_'))", T --> T, "", [0], max_pri);
+    fun parents T = Mfix ("'(_')", T --> T, "", [0], max_pri);
 
     fun mkappl T =
       Mfix ("(1_/(1'(_')))", [funT, argsT] ---> T, applC, [max_pri, 0], max_pri);