# HG changeset patch
# User wenzelm
# Date 962473271 -7200
# Node ID 0842edfc8245a203ba4123da9c92509089ef19f6
# Parent  50de4abb987c0fcea5d72e9094ac6e0f716b01bb
removed help_attributes;

diff -r 50de4abb987c -r 0842edfc8245 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Jul 01 19:40:46 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Jul 01 19:41:11 2000 +0200
@@ -16,7 +16,6 @@
 signature ATTRIB =
 sig
   include BASIC_ATTRIB
-  val help_attributes: theory option -> Pretty.T list
   exception ATTRIB_FAIL of (string * Position.T) * exn
   val global_attribute: theory -> Args.src -> theory attribute
   val local_attribute: theory -> Args.src -> Proof.context attribute
@@ -63,24 +62,19 @@
       attrs = Symtab.merge eq_snd (attrs1, attrs2) handle Symtab.DUPS dups =>
         error ("Attempt to merge different versions of attributes " ^ commas_quote dups)};
 
-  fun pretty_atts verbose ({space, attrs}) =
+  fun print _ {space, attrs} =
     let
       fun prt_attr (name, ((_, comment), _)) = Pretty.block
         [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
     in
-      (if not verbose then [] else [Display.pretty_name_space ("attribute name space", space)]) @
       [Pretty.big_list "attributes:" (map prt_attr (NameSpace.cond_extern_table space attrs))]
+      |> Pretty.chunks |> Pretty.writeln
     end;
-
-   fun print _ = Pretty.writeln o Pretty.chunks o pretty_atts true;
 end;
 
 structure AttributesData = TheoryDataFun(AttributesDataArgs);
 val print_attributes = AttributesData.print;
 
-fun help_attributes None = [Pretty.str "attributes: (unkown theory context)"]
-  | help_attributes (Some thy) = AttributesDataArgs.pretty_atts false (AttributesData.get thy);
-
 
 (* get global / local attributes *)
 
@@ -276,6 +270,7 @@
 
 fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
 fun elimify x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
+fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
 
 fun global_export x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x;
 fun local_export x = no_args (Drule.rule_attribute Proof.export_thm) x;
@@ -298,6 +293,7 @@
   ("fold", (global_fold, local_fold), "fold definitions"),
   ("standard", (standard, standard), "put theorem into standard form"),
   ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
+  ("no_vars", (no_vars, no_vars), "freeze schematic vars"),
   ("case_names", (case_names, case_names), "name rule cases"),
   ("params", (params, params), "name rule parameters"),
   ("export", (global_export, local_export), "export theorem from context")];