diff -r 972a73d7c50b -r 0be0c4e7ab9e src/Tools/isac/ProgLang/term.sml
--- a/src/Tools/isac/ProgLang/term.sml	Mon Sep 06 17:07:28 2010 +0200
+++ b/src/Tools/isac/ProgLang/term.sml	Wed Sep 08 10:15:51 2010 +0200
@@ -20,7 +20,7 @@
     (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
     handle _ => false
 
-fun atomtyp t = (*see raw_pp_typ*)
+fun atomtyp t = (*WN10 see raw_pp_typ*)
   let
     fun ato n (Type (s,[])) = 
       ("\n*** "^indent n^"Type ("^s^",[])")
@@ -37,9 +37,20 @@
       ("\n*** "^indent n^"]")
       | atol n (T::Ts) = (ato n T ^ atol n Ts)
 (*in print (ato 0 t ^ "\n") end;  TODO TUM10*)
-in writeln(ato 0 t) end;
+in writeln (ato 0 t) end;
+(*
+> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
+> atomtyp T;
+*** Type (fun,[
+***   Type (RealDef.real,[])
+***   Type (fun,[
+***     Type (IntDef.int,[])
+***     Type (nat,[])
+***     ]
+***   ]
+*)
 
-(*Prog.Tutorial.p.34*)
+(*Prog.Tutorial.p.34, Makarius 1005 does the above like this..*)
 local
    fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
    fun pp_list xs = Pretty.list "[" "]" xs
@@ -64,49 +75,37 @@
   (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy);
 *)
 
-(*
-> val T = (type_of o term_of o the o (parse thy)) "a::[real,int] => nat";
-> atomtyp T;
-*** Type (fun,[
-***   Type (RealDef.real,[])
-***   Type (fun,[
-***     Type (IntDef.int,[])
-***     Type (nat,[])
-***     ]
-***   ]
-*)
-
 fun atomt t =
-    let fun ato (Const(a,T))     n = 
-	("\n*** "^indent n^"Const ("^a^")")
-	  | ato (Free (a,T))     n =  
-	("\n*** "^indent n^"Free ("^a^", "^")")
-	  | ato (Var ((a,ix),T)) n =
-	("\n*** "^indent n^"Var (("^a^", "^(string_of_int ix)^"), "^")")
-	  | ato (Bound ix)       n = 
-	("\n*** "^indent n^"Bound "^(string_of_int ix))
-	  | ato (Abs(a,T,body))  n = 
-	("\n*** "^indent n^"Abs("^a^",..")^ato body (n+1)
-	  | ato (f$t')           n = (ato f n; ato t' (n+1))
-    in writeln("\n*** -------------"^ ato t 0 ^"\n***") end;
+    let fun ato (Const (a, _)) n = 
+	           "\n*** " ^ indent n ^ "Const (" ^ a ^ ", _)"
+	  | ato (Free (a, _)) n =  
+	           "\n*** " ^ indent n ^ "Free (" ^ a ^ ", _)"
+	  | ato (Var ((a, i), _)) n =
+	           "\n*** " ^ indent n ^ "Var (" ^ a ^ ", " ^ 
+                                               string_of_int i ^ "), _)"
+	  | ato (Bound i) n = 
+	           "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
+	  | ato (Abs (a, _, body)) n = 
+	           "\n*** " ^ indent n ^ "Abs(" ^ a ^ ", _" ^ ato body (n+1)
+	  | ato (f $ t) n = (ato f n ^ ato t (n + 1))
+    in writeln ("\n*** -------------" ^ ato t 0 ^ "\n***") end;
 
 fun term_detail2str t =
-    let fun ato (Const (a, T))     n = 
-	    "\n*** "^indent n^"Const ("^a^", "^string_of_typ T^")"
-	  | ato (Free (a, T))     n =  
-	    "\n*** "^indent n^"Free ("^a^", "^string_of_typ T^")"
-	  | ato (Var ((a, ix), T)) n =
-	    "\n*** "^indent n^"Var (("^a^", "^string_of_int ix^"), "^
-	    string_of_typ T^")"
-	  | ato (Bound ix)       n = 
-	    "\n*** "^indent n^"Bound "^string_of_int ix
+    let fun ato (Const (a, T)) n = 
+	    "\n*** " ^ indent n ^ "Const (" ^ a ^ ", " ^ string_of_typ T ^ ")"
+	  | ato (Free (a, T)) n =  
+	    "\n*** " ^ indent n ^ "Free (" ^ a ^ ", " ^ string_of_typ T ^ ")"
+	  | ato (Var ((a, i), T)) n =
+	    "\n*** " ^ indent n ^ "Var ((" ^ a ^ ", " ^ string_of_int i ^ "), "^
+	    string_of_typ T ^ ")"
+	  | ato (Bound i) n = 
+	    "\n*** " ^ indent n ^ "Bound " ^ string_of_int i
 	  | ato (Abs(a, T, body))  n = 
-	    "\n*** "^indent n^"Abs ("^a^", "^
-	       (string_of_typ T)^",.."
-	    ^ato body (n + 1)
-	  | ato (f $ t')           n = ato f n^ato t' (n+1)
-    in "\n*** "^ato t 0^"\n***" end;
-fun atomty t = (writeln o term_detail2str) t;
+	    "\n*** " ^ indent n ^ "Abs (" ^ a ^ ", " ^ string_of_typ T ^ ",.."
+	    ^ ato body (n + 1)
+	  | ato (f $ t) n = ato f n ^ ato t (n + 1)
+    in "\n*** " ^ ato t 0 ^ "\n***" end;
+fun atomty t = (writeln o term_detail2str) t; (*WN100907 broken*)
 
 fun term_str thy (Const(s,_)) = s
   | term_str thy (Free(s,_)) = s
@@ -802,98 +801,28 @@
 fun mk_Free (s,T) = Free(s,T);
 fun mk_free T s =  Free(s,T);
 
+(*Special case: one argument cp from Isabelle2002/src/Pure/term.ML*)
+fun subst_bound (arg, t) : term = (*WN100908 neglects 'raise Same.SAME'*)
+  let fun subst (t as Bound i, lev) =
+            if i<lev then  t    (*var is locally bound*)
+            else  if i=lev then incr_boundvars lev arg
+                           else Bound(i-1)  (*loose: change it*)
+        | subst (Abs(a,T,body), lev) = Abs(a, T,  subst(body,lev+1))
+        | subst (f$t, lev) =  subst(f,lev)  $  subst(t,lev)
+        | subst (t,lev) = t
+  in  subst (t,0)  end;
+
 (*instantiate let; necessary for ass_up*)
-fun inst_abs thy (Const sT) = Const sT
+fun inst_abs thy (Const sT) = Const sT  (*TODO.WN100907 drop thy*)
   | inst_abs thy (Free sT) = Free sT
   | inst_abs thy (Bound n) = Bound n
   | inst_abs thy (Var iT) = Var iT
-  | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) = 
-  let val (v',b') = variant_abs (v,T2,b);     (*fun variant_abs: term.ML*)
-  in Const ("Let",T1) $ inst_abs thy e $ (Abs (v',T2,inst_abs thy b')) end
+  | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v, T2, b))) = 
+    let val b' = subst_bound (Free (v, T2), b);
+    (*fun variant_abs: term.ML*)
+    in Const ("Let", T1) $ inst_abs thy e $ (Abs (v, T2, inst_abs thy b')) end
   | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
-  | inst_abs thy t = 
-    (writeln("inst_abs: unchanged t= "^ term2str t);
-     t);
-(*val scr as (Script sc) = Script ((term_of o the o (parse thy))
- "Script Testeq (e_::bool) =                                        \
-   \While (contains_root e_) Do                                     \
-   \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_));    \
-   \      e_ = Try (Repeat (Rewrite square_equation_left True e_)) \
-   \   in Try (Repeat (Rewrite radd_0 False e_)))                 ");
-ML> atomt sc;
-*** Const ( Script.Testeq)
-*** . Free ( e_, )
-*** . Const ( Script.While)
-*** . . Const ( RatArith.contains'_root)
-*** . . . Free ( e_, )
-*** . . Const ( Let)
-*** . . . Const ( Script.Try)
-*** . . . . Const ( Script.Repeat)
-*** . . . . . Const ( Script.Rewrite)
-*** . . . . . . Free ( rroot_square_inv, )
-*** . . . . . . Const ( False)
-*** . . . . . . Free ( e_, )
-*** . . . Abs( e_,..
-*** . . . . Const ( Let)
-*** . . . . . Const ( Script.Try)
-*** . . . . . . Const ( Script.Repeat)
-*** . . . . . . . Const ( Script.Rewrite)
-*** . . . . . . . . Free ( square_equation_left, )
-*** . . . . . . . . Const ( True)
-*** . . . . . . . . Bound 0                            <-- !!!
-*** . . . . . Abs( e_,..
-*** . . . . . . Const ( Script.Try)
-*** . . . . . . . Const ( Script.Repeat)
-*** . . . . . . . . Const ( Script.Rewrite)
-*** . . . . . . . . . Free ( radd_0, )
-*** . . . . . . . . . Const ( False)
-*** . . . . . . . . . Bound 0                          <-- !!!
-val it = () : unit
-ML> atomt (inst_abs thy sc);
-*** Const ( Script.Testeq)
-*** . Free ( e_, )
-*** . Const ( Script.While)
-*** . . Const ( RatArith.contains'_root)
-*** . . . Free ( e_, )
-*** . . Const ( Let)
-*** . . . Const ( Script.Try)
-*** . . . . Const ( Script.Repeat)
-*** . . . . . Const ( Script.Rewrite)
-*** . . . . . . Free ( rroot_square_inv, )
-*** . . . . . . Const ( False)
-*** . . . . . . Free ( e_, )
-*** . . . Abs( e_,..
-*** . . . . Const ( Let)
-*** . . . . . Const ( Script.Try)
-*** . . . . . . Const ( Script.Repeat)
-*** . . . . . . . Const ( Script.Rewrite)
-*** . . . . . . . . Free ( square_equation_left, )
-*** . . . . . . . . Const ( True)
-*** . . . . . . . . Free ( e_, )                        <-- !!!
-*** . . . . . Abs( e_,..
-*** . . . . . . Const ( Script.Try)
-*** . . . . . . . Const ( Script.Repeat)
-*** . . . . . . . . Const ( Script.Rewrite)
-*** . . . . . . . . . Free ( radd_0, )
-*** . . . . . . . . . Const ( False)
-*** . . . . . . . . . Free ( e_, )                      <-- ZUFALL vor 5.03!!!
-val it = () : unit*)
-
-
-
-
-fun inst_abs thy (Const sT) = Const sT
-  | inst_abs thy (Free sT) = Free sT
-  | inst_abs thy (Bound n) = Bound n
-  | inst_abs thy (Var iT) = Var iT
-  | inst_abs thy (Const ("Let",T1) $ e $ (Abs (v,T2,b))) = 
-  let val b' = subst_bound (Free(v,T2),b);
-  (*fun variant_abs: term.ML*)
-  in Const ("Let",T1) $ inst_abs thy e $ (Abs (v,T2,inst_abs thy b')) end
-  | inst_abs thy (t1 $ t2) = inst_abs thy t1 $ inst_abs thy t2
-  | inst_abs thy t = 
-    (writeln("inst_abs: unchanged t= "^ term2str t);
-     t);
+  | inst_abs thy t = t;
 (*val scr =    
    "Script Make_fun_by_explicit (f_::real) (v_::real) (eqs_::bool list) = \
    \ (let h_ = (hd o (filterVar f_)) eqs_;                    \