equal
deleted
inserted
replaced
150 |
150 |
151 (**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****) |
151 (**** REPLACING ABSTRACTIONS BY FUNCTION DEFINITIONS ****) |
152 |
152 |
153 (*Returns the vars of a theorem*) |
153 (*Returns the vars of a theorem*) |
154 fun vars_of_thm th = |
154 fun vars_of_thm th = |
155 map (Thm.cterm_of (theory_of_thm th) o Var) (Drule.fold_terms Term.add_vars th []); |
155 map (Thm.cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []); |
156 |
156 |
157 (*Make a version of fun_cong with a given variable name*) |
157 (*Make a version of fun_cong with a given variable name*) |
158 local |
158 local |
159 val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) |
159 val fun_cong' = fun_cong RS asm_rl; (*renumber f, g to prevent clashes with (a,0)*) |
160 val cx = hd (vars_of_thm fun_cong'); |
160 val cx = hd (vars_of_thm fun_cong'); |