equal
deleted
inserted
replaced
72 val iso_tuple_intro = @{thm isomorphic_tuple_intro}; |
72 val iso_tuple_intro = @{thm isomorphic_tuple_intro}; |
73 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros}; |
73 val iso_tuple_intros = Tactic.build_net @{thms isomorphic_tuple.intros}; |
74 |
74 |
75 val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple}); |
75 val tuple_iso_tuple = (@{const_name Record.tuple_iso_tuple}, @{thm tuple_iso_tuple}); |
76 |
76 |
77 fun named_cterm_instantiate values thm = |
77 fun named_cterm_instantiate values thm = (* FIXME eliminate *) |
78 let |
78 let |
79 fun match name ((name', _), _) = name = name'; |
79 fun match name ((name', _), _) = name = name'; |
80 fun getvar name = |
80 fun getvar name = |
81 (case find_first (match name) (Term.add_vars (prop_of thm) []) of |
81 (case find_first (match name) (Term.add_vars (prop_of thm) []) of |
82 SOME var => cterm_of (theory_of_thm thm) (Var var) |
82 SOME var => cterm_of (theory_of_thm thm) (Var var) |