1.1 --- a/src/sml/Scripts/term_G.sml	Tue Oct 28 15:16:31 2008 +0100
     1.2 +++ b/src/sml/Scripts/term_G.sml	Tue Nov 18 16:34:39 2008 +0100
     1.3 @@ -108,8 +108,17 @@
     1.4  
     1.5  (*.contains the fst argument the second argument (a leave! of term).*)
     1.6  fun contains_term (Abs(_,_,body)) t = contains_term body t 
     1.7 -  | contains_term (f $ f') t = contains_term f t orelse contains_term f' t
     1.8 +  | contains_term (f $ f') t = 
     1.9 +    contains_term f t orelse contains_term f' t
    1.10    | contains_term s t = t = s;
    1.11 +(*.contains the term a VAR(("*",_),_) ?.*)
    1.12 +fun contains_Var (Abs(_,_,body)) = contains_Var body
    1.13 +  | contains_Var (f $ f') = contains_Var f orelse contains_Var f'
    1.14 +  | contains_Var (Var _) = true
    1.15 +  | contains_Var _ = false;
    1.16 +(* contains_Var (str2term "?z = 3") (*true*);
    1.17 +   contains_Var (str2term "z = 3")  (*false*);
    1.18 +   *)
    1.19  
    1.20  (*..*)
    1.21  fun int_of_str str =
    1.22 @@ -235,7 +244,9 @@
    1.23  > cterm_of (sign_of thy) ss;
    1.24  val it = "[R = R, R = R, R = R]" : cterm  *)
    1.25  
    1.26 -fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b);
    1.27 +fun isapair2pair (Const ("Pair",_) $ a $ b) = (a,b)
    1.28 +  | isapair2pair t = 
    1.29 +    raise error ("isapair2pair called with "^term2str t);
    1.30  
    1.31  val listType = Type ("List.list",[Type ("bool",[])]);
    1.32  fun isalist2list ls =