src/Pure/Isar/interpretation.ML
changeset 68855 59ce31e15c33
parent 68854 404e04f649d4
child 69050 812e60d15172
     1.1 --- a/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:38:24 2018 +0200
     1.2 +++ b/src/Pure/Isar/interpretation.ML	Thu Aug 30 14:48:02 2018 +0200
     1.3 @@ -100,7 +100,7 @@
     1.4  fun abs_def_rule eqns ctxt =
     1.5    (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
     1.6  
     1.7 -fun note_eqns_register pos note add_registration
     1.8 +fun note_eqns_register note add_registration
     1.9      deps eqnss witss def_eqns thms export export' ctxt =
    1.10    let
    1.11      val factss = thms
    1.12 @@ -112,10 +112,7 @@
    1.13      val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
    1.14      val deps' =
    1.15        (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
    1.16 -        let val morph' = morph
    1.17 -          $> Element.satisfy_morphism (map (Element.transform_witness export') wits)
    1.18 -          $> Morphism.binding_morphism "position" (Binding.set_pos pos)
    1.19 -        in (dep, morph') end);
    1.20 +        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
    1.21      fun register (dep, eqns) ctxt =
    1.22        ctxt |> add_registration
    1.23          {dep = dep,
    1.24 @@ -132,9 +129,8 @@
    1.25    let
    1.26      val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
    1.27        prep_interpretation expression raw_defs initial_ctxt;
    1.28 -    val pos = Position.thread_data ();
    1.29      fun after_qed witss eqns =
    1.30 -      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
    1.31 +      note_eqns_register note add_registration deps eqnss witss def_eqns eqns export export';
    1.32    in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
    1.33  
    1.34  end;