equal
deleted
inserted
replaced
32 val pnames = |
32 val pnames = |
33 if length descr = 1 then ["P"] |
33 if length descr = 1 then ["P"] |
34 else map (fn i => "P" ^ string_of_int i) (1 upto length descr); |
34 else map (fn i => "P" ^ string_of_int i) (1 upto length descr); |
35 |
35 |
36 val rec_result_Ts = map (fn ((i, _), P) => |
36 val rec_result_Ts = map (fn ((i, _), P) => |
37 if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT) |
37 if member (=) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT) |
38 (descr ~~ pnames); |
38 (descr ~~ pnames); |
39 |
39 |
40 fun make_pred i T U r x = |
40 fun make_pred i T U r x = |
41 if member (op =) is i then |
41 if member (op =) is i then |
42 Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x |
42 Free (nth pnames i, T --> U --> HOLogic.boolT) $ r $ x |