equal
deleted
inserted
replaced
102 |
102 |
103 local |
103 local |
104 |
104 |
105 val mk_var = Net.encode_type o #2 o Term.dest_Var; |
105 val mk_var = Net.encode_type o #2 o Term.dest_Var; |
106 |
106 |
107 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => |
107 fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle List.Empty => |
108 raise THM ("No variables in conclusion of rule", 0, [thm]); |
108 raise THM ("No variables in conclusion of rule", 0, [thm]); |
109 |
109 |
110 in |
110 in |
111 |
111 |
112 fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle Empty => |
112 fun left_var_prem thm = mk_var (hd (vars_of (hd (Thm.prems_of thm)))) handle List.Empty => |
113 raise THM ("No variables in major premise of rule", 0, [thm]); |
113 raise THM ("No variables in major premise of rule", 0, [thm]); |
114 |
114 |
115 val left_var_concl = concl_var hd; |
115 val left_var_concl = concl_var hd; |
116 val right_var_concl = concl_var List.last; |
116 val right_var_concl = concl_var List.last; |
117 |
117 |