src/HOL/Tools/BNF/bnf_lift.ML
changeset 61072 f9be82413170
parent 61067 180a20d4ae53
child 61073 eea21f2ddf16
equal deleted inserted replaced
61071:c6ac3c3fbb85 61072:f9be82413170
    47 
    47 
    48 fun typedef_bnf thm wits specs map_b rel_b opts lthy =
    48 fun typedef_bnf thm wits specs map_b rel_b opts lthy =
    49   let
    49   let
    50     val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
    50     val plugins = get_first (fn Plugins_Option f => SOME (f lthy) | _ => NONE) (rev opts)
    51       |> the_default Plugin_Name.default_filter;
    51       |> the_default Plugin_Name.default_filter;
    52     val no_warn_wits = exists (can (fn Sequential_Option => ())) opts;
    52     val no_warn_wits = exists (fn No_Warn_Wits => true | _ => false) opts;
    53 
    53 
    54     (* extract Rep Abs F RepT AbsT *)
    54     (* extract Rep Abs F RepT AbsT *)
    55     val (_, [Rep_G, Abs_G, F]) = Thm.prop_of thm
    55     val (_, [Rep_G, Abs_G, F]) = Thm.prop_of thm
    56       |> HOLogic.dest_Trueprop
    56       |> HOLogic.dest_Trueprop
    57       |> Term.strip_comb;
    57       |> Term.strip_comb;