equal
deleted
inserted
replaced
305 fun close_form t = |
305 fun close_form t = |
306 fold (fn ((s, i), T) => fn t' => |
306 fold (fn ((s, i), T) => fn t' => |
307 Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
307 Logic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t'))) |
308 (Term.add_vars t []) t |
308 (Term.add_vars t []) t |
309 |
309 |
310 val hol_close_form_prefix = "ATP.close_form." |
310 val hol_close_form_prefix = "ATP." |
311 |
311 |
312 fun hol_close_form t = |
312 fun hol_close_form t = |
313 fold (fn ((s, i), T) => fn t' => |
313 fold (fn ((s, i), T) => fn t' => |
314 HOLogic.all_const T |
314 HOLogic.all_const T |
315 $ Abs (hol_close_form_prefix ^ s, T, |
315 $ Abs (hol_close_form_prefix ^ s, T, |