simple_ast_of: fixed handling of loose Bounds;
authorwenzelm
Mon, 31 Mar 1997 14:42:13 +0200
changeset 2848 f1cd1ad27588
parent 2847 6226b83ce2d8
child 2849 01a536a6e4fb
simple_ast_of: fixed handling of loose Bounds;
src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sun Mar 30 13:40:38 1997 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Mar 31 14:42:13 1997 +0200
@@ -67,7 +67,7 @@
       let val (f, args) = strip_comb t in
         mk_appl (simple_ast_of f) (map simple_ast_of args)
       end
-  | simple_ast_of (Bound _) = sys_error "simple_ast_of: Bound"
+  | simple_ast_of (Bound i) = Variable ("B." ^ string_of_int i)
   | simple_ast_of (Abs _) = sys_error "simple_ast_of: Abs";