diff -r 5c4230e32124 -r 80efccb7e5c1 src/Tools/isac/ProgLang/Prog_Expr.thy
--- a/src/Tools/isac/ProgLang/Prog_Expr.thy	Thu Sep 12 14:42:53 2019 +0200
+++ b/src/Tools/isac/ProgLang/Prog_Expr.thy	Fri Sep 13 18:35:51 2019 +0200
@@ -120,17 +120,15 @@
 (*+ for Or_to_List +*)
 fun or2list (Const ("HOL.True",_)) = (tracing"### or2list True";UniversalList)
   | or2list (Const ("HOL.False",_)) = (tracing"### or2list False";EmptyList)
-  | or2list (t as Const ("HOL.eq",_) $ _ $ _) = 
-    (tracing"### or2list _ = _"; TermC.list2isalist HOLogic.boolT [t])
+  | or2list (t as Const ("HOL.eq",_) $ _ $ _) = TermC.list2isalist HOLogic.boolT [t]
   | or2list ors =
-    (tracing"### or2list _ | _";
-    let fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
-	    case o2 of
-		Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
-	      | _ => ls @ [o1, o2] 
-    in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors)
-       handle _ => error ("or2list: no ORs= "^(Rule.term2str ors)) end
-	);
+    let
+      fun get ls (Const ("HOL.disj",_) $ o1 $ o2) =
+	        (case o2 of
+	         	Const ("HOL.disj",_) $ _ $ _ => get (ls @ [o1]) o2
+	        | _ => ls @ [o1, o2])
+        | get _ t = raise TERM ("or2list: missing pattern in fun.def", [t])
+    in (((TermC.list2isalist HOLogic.boolT) o (get [])) ors) end
 (*>val t = @{term True};
 > val t' = or2list t;
 > term2str t';
@@ -153,7 +151,7 @@
 
 (*. evaluate the predicate matches (match on whole term only) .*)
 (*("matches",("Prog_Expr.matches", eval_matches "#matches_")):calc*)
-fun eval_matches (thmid:string) "Prog_Expr.matches"
+fun eval_matches (_:string) "Prog_Expr.matches"
 		  (t as Const ("Prog_Expr.matches",_) $ pat $ tst) thy = 
     if TermC.matches thy tst pat
     then 
@@ -233,7 +231,7 @@
   in matchs t end;
 
 (*("matchsub",("Prog_Expr.matchsub", eval_matchsub "#matchsub_")):calc*)
-fun eval_matchsub (thmid:string) "Prog_Expr.matchsub"
+fun eval_matchsub (_:string) "Prog_Expr.matchsub"
 		  (t as Const ("Prog_Expr.matchsub",_) $ pat $ tst) thy = 
     if matchsub thy tst pat
     then 
@@ -246,7 +244,7 @@
 
 (*get the variables in an isabelle-term*)
 (*("Vars"    ,("Prog_Expr.Vars"    , eval_var "#Vars_")):calc*)
-fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const(op0,t0) $ arg)) thy = 
+fun eval_var (thmid:string) "Prog_Expr.Vars" (t as (Const _ $ arg)) thy = 
     let 
       val t' = ((TermC.list2isalist HOLogic.realT) o TermC.vars) t;
       val thmId = thmid ^ Rule.term_to_string''' thy arg;
@@ -339,25 +337,16 @@
 
 (*evaluate 'is_const'*)
 (*("is_const",("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_"))*)
-fun eval_const (thmid:string) _(*"Prog_Expr.is'_const" WN050820 diff.beh. rooteq*)
-	       (t as (Const _ $ arg)) _ = 
-    (*eval_const FIXXXXXME.WN.16.5.03 still forgets ComplexI*)
+fun eval_const (thmid:string) _ (t as (Const _ $ arg)) _ = 
     (case arg of 
-       Const (n1,_) =>
-	 SOME (TermC.mk_thmid thmid n1 "", 
-	       HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
-     | Free (n1,_) =>
-	 if TermC.is_num' n1
-	   then SOME (TermC.mk_thmid thmid n1 "", 
-		      HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
-	 else SOME (TermC.mk_thmid thmid n1 "", 
-		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
-     | Const ("Float.Float",_) =>
-       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", 
-	     HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
+       Const (n1, _) =>
+	     SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
+     | Free (n1, _) =>
+	     if TermC.is_num' n1
+	     then SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
+	     else SOME (TermC.mk_thmid thmid n1 "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
      | _ => (*NONE*)
-       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", 
-		    HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
+       SOME (TermC.mk_thmid thmid (Rule.term2str arg) "", HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False}))))
   | eval_const _ _ _ _ = NONE; 
 
 (*. evaluate binary, associative, commutative operators: *,+,^ .*)