equal
deleted
inserted
replaced
29 end |
29 end |
30 |
30 |
31 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom = |
31 fun mk_partial_termination_goal thy (FundefMResult {R, f, ... }, _, _, _) dom = |
32 let |
32 let |
33 val domT = domain_type (fastype_of f) |
33 val domT = domain_type (fastype_of f) |
34 val D = Sign.simple_read_term thy (Type.varifyT (HOLogic.mk_setT domT)) dom |
34 val D = Sign.simple_read_term thy (Logic.varifyT (HOLogic.mk_setT domT)) dom |
35 val DT = type_of D |
35 val DT = type_of D |
36 val idomT = HOLogic.dest_setT DT |
36 val idomT = HOLogic.dest_setT DT |
37 |
37 |
38 val x = Free ("x", idomT) |
38 val x = Free ("x", idomT) |
39 val z = Free ("z", idomT) |
39 val z = Free ("z", idomT) |