src/Pure/Tools/rule_insts.ML
changeset 59805 a162f779925a
parent 59801 ca948c89828e
child 59825 9fb7661651ad
equal deleted inserted replaced
59804:db0b87085c16 59805:a162f779925a
   223     val paramTs = map #2 params;
   223     val paramTs = map #2 params;
   224 
   224 
   225 
   225 
   226     (* local fixes *)
   226     (* local fixes *)
   227 
   227 
   228     val (fixed, fixes_ctxt) = param_ctxt
   228     val fixes_ctxt = param_ctxt
   229       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes;
   229       |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
   230 
   230 
   231     val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm mixed_insts fixes_ctxt;
   231     val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm mixed_insts fixes_ctxt;
       
   232 
       
   233     fun add_fixed (Free (x, _)) =
       
   234           if Variable.newly_fixed inst_ctxt param_ctxt x
       
   235           then insert (op =) x else I
       
   236       | add_fixed _ = I;
       
   237     val fixed = fold (Term.fold_aterms add_fixed o #2) inst_vars [];
   232 
   238 
   233 
   239 
   234     (* lift and instantiate rule *)
   240     (* lift and instantiate rule *)
   235 
   241 
   236     val inc = Thm.maxidx_of st + 1;
   242     val inc = Thm.maxidx_of st + 1;