src/Pure/Isar/proof.ML
changeset 70731 5b86068ffc11
parent 70730 7b5ee1fa5029
child 70732 53fa2e4e79af
equal deleted inserted replaced
70730:7b5ee1fa5029 70731:5b86068ffc11
  1055     val add_assumes =
  1055     val add_assumes =
  1056       Assumption.add_assms
  1056       Assumption.add_assms
  1057         (if strict_asm then Assumption.assume_export else Assumption.presume_export);
  1057         (if strict_asm then Assumption.assume_export else Assumption.presume_export);
  1058 
  1058 
  1059     (*params*)
  1059     (*params*)
  1060     val ((params, assumes_propss, shows_propss, result_binds, result_text), params_ctxt) = ctxt
  1060     val ((params, assumes_propss, shows_propss, result_binds, text), params_ctxt) = ctxt
  1061       |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
  1061       |> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
       
  1062 
       
  1063     val result_text = singleton (Variable.export_terms params_ctxt ctxt) text;
  1062 
  1064 
  1063     (*prems*)
  1065     (*prems*)
  1064     val (assumes_bindings, shows_bindings) =
  1066     val (assumes_bindings, shows_bindings) =
  1065       apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
  1067       apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
  1066     val (that_fact, goal_ctxt) = params_ctxt
  1068     val (that_fact, goal_ctxt) = params_ctxt