replaced ContextPosition by Position.thread_data;
authorwenzelm
Thu Jan 24 23:51:20 2008 +0100 (2008-01-24)
changeset 259599ad285dbc7a4
parent 25958 bcedde463850
child 25960 1f9956e0bd89
replaced ContextPosition by Position.thread_data;
src/Pure/Isar/theory_target.ML
src/Tools/induct.ML
     1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Jan 24 23:51:19 2008 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Jan 24 23:51:20 2008 +0100
     1.3 @@ -119,7 +119,7 @@
     1.4      val result = th''
     1.5        |> PureThy.name_thm true true ""
     1.6        |> Goal.close_result
     1.7 -      |> fold PureThy.tag_rule (ContextPosition.properties_of ctxt)
     1.8 +      |> fold PureThy.tag_rule (Position.properties_of (Position.thread_data ()))
     1.9        |> PureThy.name_thm true true name;
    1.10  
    1.11      (*import fixes*)
    1.12 @@ -206,7 +206,7 @@
    1.13  
    1.14  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((c, T), mx) lthy =
    1.15    let
    1.16 -    val pos = ContextPosition.properties_of lthy;
    1.17 +  val pos = Position.properties_of (Position.thread_data ());
    1.18      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.19      val U = map #2 xs ---> T;
    1.20      val (mx1, mx2, mx3) = fork_mixfix ta mx;
    1.21 @@ -234,7 +234,7 @@
    1.22  
    1.23  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((c, mx), t) lthy =
    1.24    let
    1.25 -    val pos = ContextPosition.properties_of lthy;
    1.26 +    val pos = Position.properties_of (Position.thread_data ());
    1.27      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.28      val target_ctxt = LocalTheory.target_of lthy;
    1.29  
     2.1 --- a/src/Tools/induct.ML	Thu Jan 24 23:51:19 2008 +0100
     2.2 +++ b/src/Tools/induct.ML	Thu Jan 24 23:51:20 2008 +0100
     2.3 @@ -308,9 +308,9 @@
     2.4  fun make_cases is_open rule =
     2.5    RuleCases.make_common is_open (Thm.theory_of_thm rule, Thm.prop_of rule);
     2.6  
     2.7 -fun warn_open ctxt true =
     2.8 -      legacy_feature ("open rule cases in proof method" ^ ContextPosition.str_of ctxt)
     2.9 -  | warn_open _ false = ();
    2.10 +fun warn_open true =
    2.11 +      legacy_feature ("open rule cases in proof method" ^ Position.str_of (Position.thread_data ()))
    2.12 +  | warn_open false = ();
    2.13  
    2.14  
    2.15  
    2.16 @@ -336,7 +336,7 @@
    2.17  
    2.18  fun cases_tac ctxt is_open insts opt_rule facts =
    2.19    let
    2.20 -    val _ = warn_open ctxt is_open;
    2.21 +    val _ = warn_open is_open;
    2.22      val thy = ProofContext.theory_of ctxt;
    2.23      val cert = Thm.cterm_of thy;
    2.24  
    2.25 @@ -575,7 +575,7 @@
    2.26  
    2.27  fun induct_tac ctxt is_open def_insts arbitrary taking opt_rule facts =
    2.28    let
    2.29 -    val _ = warn_open ctxt is_open;
    2.30 +    val _ = warn_open is_open;
    2.31      val thy = ProofContext.theory_of ctxt;
    2.32      val cert = Thm.cterm_of thy;
    2.33  
    2.34 @@ -651,7 +651,7 @@
    2.35  
    2.36  fun coinduct_tac ctxt is_open inst taking opt_rule facts =
    2.37    let
    2.38 -    val _ = warn_open ctxt is_open;
    2.39 +    val _ = warn_open is_open;
    2.40      val thy = ProofContext.theory_of ctxt;
    2.41      val cert = Thm.cterm_of thy;
    2.42