equal
deleted
inserted
replaced
98 val dummy = assert_all is_Free rec_params |
98 val dummy = assert_all is_Free rec_params |
99 (fn t => "Param in recursion term not a free variable: " ^ |
99 (fn t => "Param in recursion term not a free variable: " ^ |
100 Sign.string_of_term sign t); |
100 Sign.string_of_term sign t); |
101 |
101 |
102 (*** Construct the fixedpoint definition ***) |
102 (*** Construct the fixedpoint definition ***) |
103 val mk_variant = variant (foldr add_term_names [] intr_tms); |
103 val mk_variant = Name.variant (foldr add_term_names [] intr_tms); |
104 |
104 |
105 val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; |
105 val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w"; |
106 |
106 |
107 fun dest_tprop (Const("Trueprop",_) $ P) = P |
107 fun dest_tprop (Const("Trueprop",_) $ P) = P |
108 | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ |
108 | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^ |