src/HOL/BNF/Tools/bnf_def.ML
changeset 51767 bbcdd8519253
parent 51766 f19a4d0ab1bf
child 51787 1267c28c7bdd
     1.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 17:47:22 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Apr 24 18:49:52 2013 +0200
     1.3 @@ -94,7 +94,8 @@
     1.4    val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
     1.5      ({prems: thm list, context: Proof.context} -> tactic) list ->
     1.6      ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
     1.7 -    binding list -> ((((binding * term) * term list) * term) * term list) * term option ->
     1.8 +    binding -> binding list ->
     1.9 +    ((((binding * term) * term list) * term) * term list) * term option ->
    1.10      local_theory -> BNF * local_theory
    1.11  end;
    1.12  
    1.13 @@ -544,7 +545,7 @@
    1.14  
    1.15  (* Define new BNFs *)
    1.16  
    1.17 -fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b set_bs
    1.18 +fun prepare_def const_policy mk_fact_policy qualify prep_term Ds_opt map_b rel_b set_bs
    1.19    (((((raw_b, raw_map), raw_sets), raw_bd_Abs), raw_wits), raw_rel_opt) no_defs_lthy =
    1.20    let
    1.21      val fact_policy = mk_fact_policy no_defs_lthy;
    1.22 @@ -766,7 +767,9 @@
    1.23            (Term.list_comb (fold_rev Term.absfree Rs' O_Gr, sQs)))
    1.24        | SOME raw_rel => prep_term no_defs_lthy raw_rel);
    1.25  
    1.26 -    val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
    1.27 +    val rel_bind_def =
    1.28 +      (fn () => if Binding.is_empty rel_b then Binding.suffix_name ("_" ^ relN) b else rel_b,
    1.29 +       rel_rhs);
    1.30  
    1.31      val ((bnf_rel_term, raw_rel_def), (lthy, lthy_old)) =
    1.32        lthy
    1.33 @@ -1261,7 +1264,7 @@
    1.34  fun mk_conjunction_balanced' [] = @{prop True}
    1.35    | mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts;
    1.36  
    1.37 -fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
    1.38 +fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds map_b rel_b set_bs =
    1.39    (fn (_, goals, wit_goalss, after_qed, lthy, one_step_defs) =>
    1.40    let
    1.41      val wits_tac =
    1.42 @@ -1277,13 +1280,14 @@
    1.43      map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
    1.44        goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
    1.45      |> (fn thms => after_qed (map single thms @ wit_thms) lthy)
    1.46 -  end) oooo prepare_def const_policy fact_policy qualify (K I) Ds;
    1.47 +  end) oo prepare_def const_policy fact_policy qualify (K I) Ds map_b rel_b set_bs;
    1.48  
    1.49  val bnf_def_cmd = (fn (key, goals, wit_goals, after_qed, lthy, defs) =>
    1.50    Proof.unfolding ([[(defs, [])]])
    1.51      (Proof.theorem NONE (snd o register_bnf key oo after_qed)
    1.52        (map (single o rpair []) goals @ map (map (rpair [])) wit_goals) lthy)) oo
    1.53 -  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty [];
    1.54 +  prepare_def Do_Inline (user_policy Note_Some) I Syntax.read_term NONE Binding.empty Binding.empty
    1.55 +    [];
    1.56  
    1.57  fun print_bnfs ctxt =
    1.58    let