src/Pure/Isar/generic_target.ML
changeset 47292 1884d34e9aab
parent 47291 6a641856a0e9
child 47293 052cd5f1a591
equal deleted inserted replaced
47291:6a641856a0e9 47292:1884d34e9aab
   192 
   192 
   193 fun abbrev target_abbrev prmode ((b, mx), t) lthy =
   193 fun abbrev target_abbrev prmode ((b, mx), t) lthy =
   194   let
   194   let
   195     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
   195     val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy);
   196 
   196 
   197     val t' = Assumption.export_term lthy thy_ctxt t;
   197     val t' = Assumption.export_term lthy (Local_Theory.target_of lthy) t;
   198     val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' []));
   198     val xs = map Free (sort (Variable.fixed_ord lthy o pairself #1) (Variable.add_fixed lthy t' []));
   199     val u = fold_rev lambda xs t';
   199     val u = fold_rev lambda xs t';
   200     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
   200     val global_rhs = singleton (Variable.polymorphic thy_ctxt) u;
   201 
   201 
   202     val extra_tfrees =
   202     val extra_tfrees =