equal
deleted
inserted
replaced
7 |
7 |
8 (* |
8 (* |
9 > cterm_of (sign_of thy) a_term; |
9 > cterm_of (sign_of thy) a_term; |
10 val it = "empty" : cterm *) |
10 val it = "empty" : cterm *) |
11 |
11 |
12 (*1003 fun match thy t pat = |
12 (*2003 fun match thy t pat = |
13 (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))) |
13 (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t))) |
14 handle _ => []; |
14 handle _ => []; |
15 fn : theory -> |
15 fn : theory -> |
16 Term.term -> Term.term -> (Term.indexname * Term.term) list*) |
16 Term.term -> Term.term -> (Term.indexname * Term.term) list*) |
17 (*see src/Tools/eqsubst.ML fun clean_match*) |
17 (*see src/Tools/eqsubst.ML fun clean_match*) |
18 (*1003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*) |
18 (*2003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*) |
19 fun matches thy tm pa = |
19 fun matches thy tm pa = |
20 (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true) |
20 (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true) |
21 handle _ => false |
21 handle _ => false |
22 |
22 |
23 fun atomtyp t = (*see raw_pp_typ*) |
23 fun atomtyp t = (*see raw_pp_typ*) |