src/Pure/Isar/expression.ML
changeset 54740 91f54d386680
parent 54566 5f3e9baa8f13
child 54742 7a86358a3c0b
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 13 14:58:47 2013 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 13 20:20:15 2013 +0100
     1.3 @@ -171,7 +171,7 @@
     1.4  
     1.5  (* Instantiation morphism *)
     1.6  
     1.7 -fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
     1.8 +fun inst_morphism (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
     1.9    let
    1.10      (* parameters *)
    1.11      val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
    1.12 @@ -192,7 +192,7 @@
    1.13      val inst = Symtab.make insts'';
    1.14    in
    1.15      (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
    1.16 -      Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
    1.17 +      Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
    1.18    end;
    1.19  
    1.20  
    1.21 @@ -299,7 +299,7 @@
    1.22    let
    1.23      val thy = Proof_Context.theory_of ctxt;
    1.24      val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
    1.25 -    val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
    1.26 +    val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst) ctxt;
    1.27    in (loc, morph) end;
    1.28  
    1.29  fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
    1.30 @@ -368,7 +368,7 @@
    1.31          val insts' = insts @ [(loc, (prfx, inst''))];
    1.32          val (insts'', _, _, _) = check_autofix insts' [] [] ctxt;
    1.33          val inst''' = insts'' |> List.last |> snd |> snd;
    1.34 -        val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst''') ctxt;
    1.35 +        val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
    1.36          val ctxt'' = Locale.activate_declarations (loc, morph) ctxt;
    1.37        in (i + 1, insts', ctxt'') end;
    1.38  
    1.39 @@ -513,7 +513,8 @@
    1.40      val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
    1.41      val exp_typ = Logic.type_map exp_term;
    1.42      val export' =
    1.43 -      Morphism.morphism {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
    1.44 +      Morphism.morphism "Expression.prep_goal"
    1.45 +        {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]};
    1.46    in ((propss, deps, export'), goal_ctxt) end;
    1.47  
    1.48  in