# HG changeset patch
# User wenzelm
# Date 1450195030 -3600
# Node ID d273c24b577626427c8d04f0320a7279653f6bb6
# Parent  ccf2df82b2d30f3f9a76a4175484306445fdde9b
tuned signature -- clarified modules;

diff -r ccf2df82b2d3 -r d273c24b5776 src/HOL/Eisbach/eisbach_rule_insts.ML
--- a/src/HOL/Eisbach/eisbach_rule_insts.ML	Tue Dec 15 16:01:57 2015 +0100
+++ b/src/HOL/Eisbach/eisbach_rule_insts.ML	Tue Dec 15 16:57:10 2015 +0100
@@ -245,8 +245,8 @@
           val read_insts = read_of_insts (not unchecked) context args;
         in
           Thm.rule_attribute (fn context => fn thm =>
-            if Method_Closure.is_free_thm thm andalso unchecked
-            then Method_Closure.dummy_free_thm
+            if Thm.is_free_dummy thm andalso unchecked
+            then Drule.free_dummy_thm
             else read_instantiate_closed (Context.proof_of context) (read_insts thm) thm)
         end))
       "positional instantiation of theorem");
diff -r ccf2df82b2d3 -r d273c24b5776 src/HOL/Eisbach/match_method.ML
--- a/src/HOL/Eisbach/match_method.ML	Tue Dec 15 16:01:57 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Tue Dec 15 16:57:10 2015 +0100
@@ -171,7 +171,7 @@
                   val param_thm = map (Drule.mk_term o Thm.cterm_of ctxt' o Free) abs_nms
                     |> Conjunction.intr_balanced
                     |> Drule.generalize ([], map fst abs_nms)
-                    |> Method_Closure.tag_free_thm;
+                    |> Thm.tag_free_dummy;
 
                   val atts = map (Attrib.attribute ctxt') att;
                   val (param_thm', ctxt'') = Thm.proof_attributes atts param_thm ctxt';
@@ -183,7 +183,7 @@
 
                   val [head_thm, body_thm] =
                     Drule.zero_var_indexes_list (map label_thm [param_thm, param_thm'])
-                    |> map Method_Closure.tag_free_thm;
+                    |> map Thm.tag_free_dummy;
 
                   val ctxt''' =
                     Attrib.local_notes "" [((b, []), [([body_thm], [])])] ctxt''
diff -r ccf2df82b2d3 -r d273c24b5776 src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue Dec 15 16:01:57 2015 +0100
+++ b/src/HOL/Eisbach/method_closure.ML	Tue Dec 15 16:57:10 2015 +0100
@@ -10,9 +10,6 @@
 
 signature METHOD_CLOSURE =
 sig
-  val tag_free_thm: thm -> thm
-  val is_free_thm: thm -> bool
-  val dummy_free_thm: thm
   val wrap_attribute: {handle_all_errs : bool, declaration : bool} ->
     Binding.binding -> theory -> theory
   val read: Proof.context -> Token.src -> Method.text
@@ -69,13 +66,6 @@
 
 (* free thm *)
 
-val free_thmN = "Method_Closure.free_thm";
-fun tag_free_thm thm = Thm.tag_rule (free_thmN, "") thm;
-
-val dummy_free_thm = tag_free_thm Drule.dummy_thm;
-
-fun is_free_thm thm = Properties.defined (Thm.get_tags thm) free_thmN;
-
 fun free_aware_attribute thy {handle_all_errs, declaration} src (context, thm) =
   let
     val src' = map Token.init_assignable src;
@@ -90,9 +80,9 @@
       |> map_filter (fn (Token.Fact (_, f)) => SOME f | _ => NONE)
       |> flat;
   in
-    if exists is_free_thm (thm :: thms) then
+    if exists Thm.is_free_dummy (thm :: thms) then
       if declaration then (NONE, NONE)
-      else (NONE, SOME dummy_free_thm)
+      else (NONE, SOME Drule.free_dummy_thm)
     else apply_att thm
   end;
 
@@ -241,7 +231,7 @@
 fun dummy_named_thm named_thm ctxt =
   let
     val ctxt' = empty_named_thm named_thm ctxt;
-    val (_, ctxt'') = Thm.proof_attributes [Named_Theorems.add named_thm] dummy_free_thm ctxt';
+    val (_, ctxt'') = Thm.proof_attributes [Named_Theorems.add named_thm] Drule.free_dummy_thm ctxt';
   in ctxt'' end;
 
 fun parse_method_args method_names =
diff -r ccf2df82b2d3 -r d273c24b5776 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Dec 15 16:01:57 2015 +0100
+++ b/src/Pure/drule.ML	Tue Dec 15 16:57:10 2015 +0100
@@ -94,6 +94,7 @@
   val cterm_add_frees: cterm -> cterm list -> cterm list
   val cterm_add_vars: cterm -> cterm list -> cterm list
   val dummy_thm: thm
+  val free_dummy_thm: thm
   val is_sort_constraint: term -> bool
   val sort_constraintI: thm
   val sort_constraint_eq: thm
@@ -628,6 +629,7 @@
 val cterm_add_vars = Thm.add_vars o mk_term;
 
 val dummy_thm = mk_term (certify Term.dummy_prop);
+val free_dummy_thm = Thm.tag_free_dummy dummy_thm;
 
 
 (* sort_constraint *)
diff -r ccf2df82b2d3 -r d273c24b5776 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Dec 15 16:01:57 2015 +0100
+++ b/src/Pure/more_thm.ML	Tue Dec 15 16:57:10 2015 +0100
@@ -97,6 +97,8 @@
   val untag_rule: string -> thm -> thm
   val tag: string * string -> attribute
   val untag: string -> attribute
+  val is_free_dummy: thm -> bool
+  val tag_free_dummy: thm -> thm
   val def_name: string -> string
   val def_name_optional: string -> string -> string
   val def_binding: Binding.binding -> Binding.binding
@@ -584,6 +586,13 @@
 fun untag s = rule_attribute (K (untag_rule s));
 
 
+(* free dummy thm -- for abstract closure *)
+
+val free_dummyN = "free_dummy";
+fun is_free_dummy thm = Properties.defined (Thm.get_tags thm) free_dummyN;
+val tag_free_dummy = tag_rule (free_dummyN, "");
+
+
 (* def_name *)
 
 fun def_name c = c ^ "_def";