1.1 --- a/src/Tools/isac/Scripts/term_G.sml	Thu Aug 19 15:41:56 2010 +0200
     1.2 +++ b/src/Tools/isac/Scripts/term_G.sml	Fri Aug 20 12:25:37 2010 +0200
     1.3 @@ -9,13 +9,13 @@
     1.4  > cterm_of (sign_of thy) a_term;
     1.5  val it = "empty" : cterm        *)
     1.6  
     1.7 -(*1003 fun match thy t pat =
     1.8 +(*2003 fun match thy t pat =
     1.9      (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)))
    1.10      handle _ => [];
    1.11  fn : theory ->
    1.12       Term.term -> Term.term -> (Term.indexname * Term.term) list*)
    1.13  (*see src/Tools/eqsubst.ML fun clean_match*)
    1.14 -(*1003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
    1.15 +(*2003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
    1.16  fun matches thy tm pa = 
    1.17      (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
    1.18      handle _ => false