equal
deleted
inserted
replaced
29 |
29 |
30 fun lookup thy net t = |
30 fun lookup thy net t = |
31 case Item_Net.retrieve net t of |
31 case Item_Net.retrieve net t of |
32 [] => NONE |
32 [] => NONE |
33 | [(f, p)] => |
33 | [(f, p)] => |
34 let |
34 SOME (Envir.subst_term (Pattern.match thy (f, t) (Vartab.empty, Vartab.empty)) p) |
35 val subst = Pattern.match thy (f, t) (Vartab.empty, Vartab.empty) |
35 handle Pattern.MATCH => NONE |
36 in |
|
37 SOME (Envir.subst_term subst p) |
|
38 end |
|
39 | _ => NONE |
36 | _ => NONE |
40 |
37 |
41 fun pred_of_function thy name = |
38 fun pred_of_function thy name = |
42 case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of |
39 case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of |
43 [] => NONE |
40 [] => NONE |