src/Pure/Isar/local_defs.ML
changeset 23541 f8c5e218e4d8
parent 22900 f8a7c10e1bd0
child 24039 273698405054
     1.1 --- a/src/Pure/Isar/local_defs.ML	Tue Jul 03 17:17:15 2007 +0200
     1.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Jul 03 17:17:15 2007 +0200
     1.3 @@ -20,6 +20,7 @@
     1.4    val print_rules: Proof.context -> unit
     1.5    val defn_add: attribute
     1.6    val defn_del: attribute
     1.7 +  val meta_rewrite_conv: Proof.context -> conv
     1.8    val meta_rewrite_rule: Proof.context -> thm -> thm
     1.9    val unfold: Proof.context -> thm list -> thm -> thm
    1.10    val unfold_goals: Proof.context -> thm list -> thm -> thm
    1.11 @@ -167,14 +168,11 @@
    1.12    MetaSimplifier.theory_context ProtoPure.thy MetaSimplifier.empty_ss
    1.13      addeqcongs [Drule.equals_cong];    (*protect meta-level equality*)
    1.14  
    1.15 -fun meta_rewrite ctxt =
    1.16 +fun meta_rewrite_conv ctxt =
    1.17    MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
    1.18      (equals_ss addsimps (Rules.get (Context.Proof ctxt)));
    1.19  
    1.20 -val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite;
    1.21 -
    1.22 -fun meta_rewrite_tac ctxt i =
    1.23 -  PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (meta_rewrite ctxt)));
    1.24 +val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite_conv;
    1.25  
    1.26  
    1.27  (* rewriting with object-level rules *)
    1.28 @@ -194,7 +192,7 @@
    1.29    let
    1.30      val ((c, T), rhs) = prop
    1.31        |> Thm.cterm_of (ProofContext.theory_of ctxt)
    1.32 -      |> meta_rewrite ctxt
    1.33 +      |> meta_rewrite_conv ctxt
    1.34        |> (snd o Logic.dest_equals o Thm.prop_of)
    1.35        |> conditional ? Logic.strip_imp_concl
    1.36        |> (abs_def o #2 o cert_def ctxt);
    1.37 @@ -204,8 +202,8 @@
    1.38            if Variable.is_fixed ctxt' x then I else insert (op =) x | _ => I) prop [];
    1.39        in
    1.40          Goal.prove ctxt' frees [] prop (K (ALLGOALS
    1.41 -          (meta_rewrite_tac ctxt' THEN'
    1.42 -            Goal.rewrite_goal_tac [def] THEN'
    1.43 +          (CONVERSION (meta_rewrite_conv ctxt') THEN'
    1.44 +            MetaSimplifier.rewrite_goal_tac [def] THEN'
    1.45              resolve_tac [Drule.reflexive_thm])))
    1.46          handle ERROR msg => cat_error msg "Failed to prove definitional specification."
    1.47        end;