src/HOL/Tools/record.ML
changeset 38252 175a5b4b2c94
parent 38012 3ca193a6ae5a
child 38401 c4de81b7fdec
equal deleted inserted replaced
38251:ea417f69b36f 38252:175a5b4b2c94
    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)