src/Pure/pattern.ML
changeset 46857 628b4a3fbf6e
parent 46219 426ed18eba43
child 51700 c8f2bad67dbb
equal deleted inserted replaced
46856:28909eecdf5b 46857:628b4a3fbf6e
   397   val envir' = apfst (typ_match thy (pT, oT)) envir;
   397   val envir' = apfst (typ_match thy (pT, oT)) envir;
   398 in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
   398 in mtch [] po envir' handle Pattern => first_order_match thy po envir' end;
   399 
   399 
   400 fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
   400 fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;
   401 
   401 
   402 fun matchess thy pos = (fold (match thy) (op ~~ pos) (Vartab.empty, Vartab.empty); true) handle MATCH => false;
   402 fun matchess thy (ps, os) =
       
   403   length ps = length os andalso
       
   404     ((fold (match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) handle MATCH => false);
   403 
   405 
   404 fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
   406 fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);
   405 
   407 
   406 
   408 
   407 (* Does pat match a subterm of obj? *)
   409 (* Does pat match a subterm of obj? *)