equal
deleted
inserted
replaced
94 |
94 |
95 fun prepare_clause parse_prop ctxt thesis vars raw_props = |
95 fun prepare_clause parse_prop ctxt thesis vars raw_props = |
96 let |
96 let |
97 val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars; |
97 val (xs', ctxt') = ctxt |> Proof_Context.add_fixes vars; |
98 val xs = map (Variable.check_name o #1) vars; |
98 val xs = map (Variable.check_name o #1) vars; |
99 |
|
100 val default_name = AList.lookup (op =) (xs' ~~ xs); |
|
101 val default_type = Variable.default_type ctxt'; |
|
102 in |
99 in |
103 Logic.list_implies (map (parse_prop ctxt') raw_props, thesis) |
100 Logic.list_implies (map (parse_prop ctxt') raw_props, thesis) |
104 |> Element.close_form ctxt default_name default_type |
101 |> fold_rev (Logic.all_constraint (Variable.default_type ctxt')) (xs ~~ xs') |
105 end; |
102 end; |
106 |
103 |
107 fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains = |
104 fun prepare_obtains prep_var parse_prop ctxt thesis raw_obtains = |
108 let |
105 let |
109 val all_types = |
106 val all_types = |