import_export_proof: simplified thm definition -- PureThy.name_thm does the job;
authorwenzelm
Sat Jun 21 16:18:52 2008 +0200 (2008-06-21)
changeset 273155d24085e0858
parent 27314 fce7f0c7cf76
child 27316 9e74019041d4
import_export_proof: simplified thm definition -- PureThy.name_thm does the job;
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sat Jun 21 16:18:51 2008 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Jun 21 16:18:52 2008 +0200
     1.3 @@ -117,10 +117,7 @@
     1.4        |> Drule.zero_var_indexes_list;
     1.5  
     1.6      (*thm definition*)
     1.7 -    val result = th''
     1.8 -      |> PureThy.name_thm true true ""
     1.9 -      |> fold PureThy.tag_rule (Position.properties_of (Position.thread_data ()))
    1.10 -      |> PureThy.name_thm true true name;
    1.11 +    val result = PureThy.name_thm true true name th'';
    1.12  
    1.13      (*import fixes*)
    1.14      val (tvars, vars) =