Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/drule.ML
changeset 59859 f9d1442c70f3
parent 59773 3adf5d1c02f6
child 59995 e79bc66572df 
--- a/src/Pure/drule.ML	Mon Mar 30 22:34:59 2015 +0200
+++ b/src/Pure/drule.ML	Tue Mar 31 00:11:54 2015 +0200
@@ -599,11 +599,11 @@
 val protect = Thm.apply (certify Logic.protectC);
 
 val protectI =
-  store_standard_thm (Binding.conceal (Binding.make ("protectI", @{here})))
+  store_standard_thm (Binding.concealed (Binding.make ("protectI", @{here})))
     (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
 
 val protectD =
-  store_standard_thm (Binding.conceal (Binding.make ("protectD", @{here})))
+  store_standard_thm (Binding.concealed (Binding.make ("protectD", @{here})))
     (Thm.equal_elim prop_def (Thm.assume (protect A)));
 
 val protect_cong =
@@ -622,7 +622,7 @@
 (* term *)
 
 val termI =
-  store_standard_thm (Binding.conceal (Binding.make ("termI", @{here})))
+  store_standard_thm (Binding.concealed (Binding.make ("termI", @{here})))
     (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
 
 fun mk_term ct =
@@ -648,11 +648,11 @@
 (* sort_constraint *)
 
 val sort_constraintI =
-  store_standard_thm (Binding.conceal (Binding.make ("sort_constraintI", @{here})))
+  store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", @{here})))
     (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
 
 val sort_constraint_eq =
-  store_standard_thm (Binding.conceal (Binding.make ("sort_constraint_eq", @{here})))
+  store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
     (Thm.equal_intr
       (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
         (Thm.unvarify_global sort_constraintI)))
isabelle