src/Pure/Isar/code.ML
changeset 66127 0561ac527270
parent 66126 60bf6934fabd
child 66128 0181bb24bdca
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.3 @@ -784,15 +784,17 @@
     1.4          val cert_thm = Conjunction.intr_balanced (map rewrite_head thms');
     1.5        in Equations (cert_thm, propers) end;
     1.6  
     1.7 -fun cert_of_proj thy c tyco =
     1.8 +fun cert_of_proj ctxt c tyco =
     1.9    let
    1.10 +    val thy = Proof_Context.theory_of ctxt
    1.11      val (vs, ((abs, (_, ty)), (rep, _))) = get_abstype_spec thy tyco;
    1.12      val _ = if c = rep then () else
    1.13        error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
    1.14    in Projection (mk_proj tyco vs ty abs rep, tyco) end;
    1.15  
    1.16 -fun cert_of_abs thy tyco c raw_abs_thm =
    1.17 +fun cert_of_abs ctxt tyco c raw_abs_thm =
    1.18    let
    1.19 +    val thy = Proof_Context.theory_of ctxt;
    1.20      val abs_thm = singleton (canonize_thms thy) raw_abs_thm;
    1.21      val _ = assert_abs_eqn thy (SOME tyco) abs_thm;
    1.22      val _ = if c = const_abs_eqn thy abs_thm then ()
    1.23 @@ -940,20 +942,16 @@
    1.24    end;
    1.25  
    1.26  fun get_cert ctxt functrans c =
    1.27 -  let
    1.28 -    val thy = Proof_Context.theory_of ctxt;
    1.29 -  in
    1.30 -    case retrieve_raw thy c of
    1.31 -      Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
    1.32 -        |> cert_of_eqns_preprocess ctxt functrans c
    1.33 -    | Eqns eqns => eqns
    1.34 -        |> cert_of_eqns_preprocess ctxt functrans c
    1.35 -    | Unimplemented => nothing_cert ctxt c
    1.36 -    | Proj ((_, tyco), _) => cert_of_proj thy c tyco
    1.37 -    | Abstr ((abs_thm, tyco), _) => abs_thm
    1.38 -       |> preprocess Conv.arg_conv ctxt
    1.39 -       |> cert_of_abs thy tyco c
    1.40 -  end;
    1.41 +  case retrieve_raw (Proof_Context.theory_of ctxt) c of
    1.42 +    Eqns_Default (_, eqns_lazy) => Lazy.force eqns_lazy
    1.43 +      |> cert_of_eqns_preprocess ctxt functrans c
    1.44 +  | Eqns eqns => eqns
    1.45 +      |> cert_of_eqns_preprocess ctxt functrans c
    1.46 +  | Unimplemented => nothing_cert ctxt c
    1.47 +  | Proj ((_, tyco), _) => cert_of_proj ctxt c tyco
    1.48 +  | Abstr ((abs_thm, tyco), _) => abs_thm
    1.49 +     |> preprocess Conv.arg_conv ctxt
    1.50 +     |> cert_of_abs ctxt tyco c;
    1.51  
    1.52  
    1.53  (* cases *)