src/Pure/Isar/obtain.ML
changeset 29006 abe0f11cfa4e
parent 28965 1de908189869
child 29383 223f18cfbb32
     1.1 --- a/src/Pure/Isar/obtain.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/Pure/Isar/obtain.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -122,7 +122,7 @@
     1.4      (*obtain vars*)
     1.5      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     1.6      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
     1.7 -    val xs = map (Name.name_of o #1) vars;
     1.8 +    val xs = map (Binding.base_name o #1) vars;
     1.9  
    1.10      (*obtain asms*)
    1.11      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
    1.12 @@ -261,7 +261,7 @@
    1.13  
    1.14  fun inferred_type (binding, _, mx) ctxt =
    1.15    let
    1.16 -    val x = Name.name_of binding;
    1.17 +    val x = Binding.base_name binding;
    1.18      val (T, ctxt') = ProofContext.inferred_param x ctxt
    1.19    in ((x, T, mx), ctxt') end;
    1.20